let p be prime Element of NAT ; :: thesis: for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds
p |^ 2 divides n
let a, b be non zero Element of NAT ; :: thesis: ( a,b are_relative_prime & p |^ 2 divides a * b & not p |^ 2 divides a implies p |^ 2 divides b )
assume A1: ( a,b are_relative_prime & p |^ 2 divides a * b ) ; :: thesis: ( p |^ 2 divides a or p |^ 2 divides b )
p divides p |^ 2 by NAT_3:3;
then A2: p divides a * b by A1, NAT_D:4;

per cases ( p divides a or p divides b ) by A2, NEWTON:98;

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

then A3: not p divides b by A1, PYTHTRIP:def 2;
p,b are_relative_prime

proof

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

end;

then p * p,b are_relative_prime by EULER_1:15;
then p |^ 2,b are_relative_prime by WSIERP_1:2;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A1, EULER_1:14; :: thesis: verum

end;

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

then A5: not p divides a by A1, PYTHTRIP:def 2;
p,a are_relative_prime

proof

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

end;

then p * p,a are_relative_prime by EULER_1:15;
then p |^ 2,a are_relative_prime by WSIERP_1:2;
hence ( p |^ 2 divides a or p |^ 2 divides b ) by A1, EULER_1:14; :: thesis: verum

end;

end;