let p be Prime; :: thesis: for m, n being non zero Nat st m,n are_coprime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n
let a, b be non zero Nat; :: thesis: ( a,b are_coprime & p |^ 2 divides a * b & not p |^ 2 divides a implies p |^ 2 divides b )
assume that
A1: a,b are_coprime and
A2: p |^ 2 divides a * b ; :: thesis: ( p |^ 2 divides a or p |^ 2 divides b )
p divides p |^ 2 by NAT_3:3;
then A3: p divides a * b by A2, NAT_D:4;

per cases ( p divides a or p divides b ) by A3, NEWTON:80;

suppose p divides a ; :: thesis: ( p |^ 2 divides a or p |^ 2 divides b )

then A4: not p divides b by A1, PYTHTRIP:def 2;
p,b are_coprime

proof

reconsider k = p gcd b as Element of NAT by ORDINAL1:def 12;
assume not p,b are_coprime ; :: thesis: contradiction
then A5: k <> 1 by INT_2:def 3;
( k divides p & k divides b ) by NAT_D:def 5;
hence contradiction by A4, A5, INT_2:def 4; :: thesis: verum

end;

then p * p,b are_coprime by EULER_1:14;
then p |^ 2,b are_coprime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; :: thesis: verum

end;

suppose p divides b ; :: thesis: ( p |^ 2 divides a or p |^ 2 divides b )

then A6: not p divides a by A1, PYTHTRIP:def 2;
p,a are_coprime

proof

reconsider k = p gcd a as Element of NAT by ORDINAL1:def 12;
assume not p,a are_coprime ; :: thesis: contradiction
then A7: k <> 1 by INT_2:def 3;
( k divides p & k divides a ) by NAT_D:def 5;
hence contradiction by A6, A7, INT_2:def 4; :: thesis: verum

end;

then p * p,a are_coprime by EULER_1:14;
then p |^ 2,a are_coprime by WSIERP_1:1;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A2, EULER_1:13; :: thesis: verum

end;

end;