let n, k be Nat; :: thesis: for a being non trivial Nat st k > 0 & Py (a,k) divides Py (a,n) holds
k divides n
let a be non trivial Nat; :: thesis: ( k > 0 & Py (a,k) divides Py (a,n) implies k divides n )
set Pk = Py (a,k);
set Pn = Py (a,n);
set r = n mod k;
set q = n div k;
assume A1: ( k > 0 & Py (a,k) divides Py (a,n) ) ; :: thesis: k divides n
reconsider r = n mod k, q = n div k as Element of NAT ;
A2: r = n - (q * k) by A1, INT_1:def 10;
then n = r + (q * k) ;
then (sgn n) * (Py (a,|.n.|)) = (((Px (a,|.r.|)) * (sgn (q * k))) * (Py (a,|.(q * k).|))) + (((sgn r) * (Py (a,|.r.|))) * (Px (a,|.(q * k).|))) by Th25;
then A3: Py (a,n) = ((Px (a,|.r.|)) * ((sgn (q * k)) * (Py (a,|.(q * k).|)))) + (((sgn r) * (Py (a,|.r.|))) * (Px (a,|.(q * k).|))) by Th23
.= ((Px (a,|.r.|)) * (Py (a,(q * k)))) + (((sgn r) * (Py (a,|.r.|))) * (Px (a,|.(q * k).|))) by Th23
.= ((Px (a,r)) * (Py (a,(q * k)))) + ((Py (a,r)) * (Px (a,(q * k)))) by Th23 ;
A4: Py (a,k) divides Py (a,(q * k)) by Th37;
Py (a,k) divides (Px (a,r)) * (Py (a,(q * k))) by Th37, INT_2:2;
then A5: Py (a,k) divides (Py (a,r)) * (Px (a,(q * k))) by INT_2:1, A1, A3;
A6: Py (a,k), Px (a,(k * q)) are_coprime
proof
(Py (a,k)) gcd (Px (a,(k * q))) divides Py (a,k) by INT_2:def 2;
then A7: (Py (a,k)) gcd (Px (a,(k * q))) divides Py (a,(q * k)) by A4, INT_2:9;
(Py (a,k)) gcd (Px (a,(k * q))) divides Px (a,(k * q)) by INT_2:def 2;
then (Py (a,k)) gcd (Px (a,(k * q))) divides (Py (a,(q * k))) gcd (Px (a,(k * q))) by A7, INT_2:22;
then (Py (a,k)) gcd (Px (a,(k * q))) divides 1 by Th26, INT_2:def 3;
then (Py (a,k)) gcd (Px (a,(k * q))) = 1 by INT_2:13;
hence Py (a,k), Px (a,(k * q)) are_coprime by INT_2:def 3; :: thesis: verum
end;
r = 0
proof
assume r <> 0 ; :: thesis: contradiction
then |.(Py (a,k)).| <= |.(Py (a,r)).| by A6, INT_4:6, A5, INT_2:25;
hence contradiction by Th14, INT_1:58, A1; :: thesis: verum
end;
hence k divides n by A2, INT_1:def 3; :: thesis: verum