let n, k be Nat; 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; ( 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) )
; 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;
verum
end;
r = 0
hence
k divides n
by A2, INT_1:def 3; verum