let n, k be Nat; for a being non trivial Nat st (Py (a,k)) ^2 divides Py (a,n) holds
Py (a,k) divides n
let a be non trivial Nat; ( (Py (a,k)) ^2 divides Py (a,n) implies Py (a,k) divides n )
assume A1:
(Py (a,k)) ^2 divides Py (a,n)
; Py (a,k) divides n
per cases
( k = 0 or k > 0 )
;
suppose A2:
k > 0
;
Py (a,k) divides n
Py (
a,
k)
divides (Py (a,k)) ^2
by INT_1:def 3;
then
Py (
a,
k)
divides Py (
a,
n)
by A1, INT_2:9;
then consider w being
Nat such that A3:
k * w = n
by NAT_D:def 3, Th39, A2;
A4:
w divides n
by A3, NAT_D:def 3;
(Py (a,k)) ^2 divides (Py (a,n)) - 0
by A1;
then A5:
0 ,
Py (
a,
n)
are_congruent_mod (Py (a,k)) ^2
by INT_1:14, INT_1:def 4;
Py (
a,
n),
(w * ((Px (a,k)) |^ (w -' 1))) * (Py (a,k)) are_congruent_mod (Py (a,k)) ^2
by Th38, A3;
then A6:
0 * ((Px (a,k)) |^ (w -' 1)),
(w * (Py (a,k))) * ((Px (a,k)) |^ (w -' 1)) are_congruent_mod (Py (a,k)) ^2
by A5, INT_1:15;
A7:
(
Py (
a,
k)
in NAT &
w in NAT )
by ORDINAL1:def 12;
A8:
(Py (a,k)) ^2 =
(Py (a,k)) * ((Py (a,k)) |^ 1)
.=
(Py (a,k)) |^ (1 + 1)
by NEWTON:6
;
Py (
a,
k),
Px (
a,
k)
are_coprime
by Th26;
then
(Py (a,k)) |^ 2,
Px (
a,
k)
are_coprime
by WSIERP_1:10;
then
0 ,
w * (Py (a,k)) are_congruent_mod (Py (a,k)) ^2
by A6, A8, INT_4:9, WSIERP_1:10;
then
(Py (a,k)) ^2 divides (w * (Py (a,k))) - 0
by INT_1:def 4, INT_1:14;
then
(
Py (
a,
k)
divides w or
Py (
a,
k)
= 0 )
by A7, PYTHTRIP:7;
hence
Py (
a,
k)
divides n
by A4, A2, INT_2:9;
verum end;