let a, b, n be Nat; :: thesis: for p being Prime st a,b are_coprime & p |^ n divides a * b & not p |^ n divides a holds
p |^ n divides b
let p be Prime; :: thesis: ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b )

per cases ( a = 0 or b = 0 or n = 0 or ( a <> 0 & b <> 0 & n <> 0 ) ) ;

suppose ( a = 0 or b = 0 ) ; :: thesis: ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b )

hence ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b ) ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b )

then p |^ n = 1 by NEWTON:4;
hence ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b ) by INT_2:12; :: thesis: verum

end;

suppose that A1: a <> 0 and
A2: b <> 0 and
A3: n <> 0 ; :: thesis: ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a implies p |^ n divides b )

assume A4: ( a,b are_coprime & p |^ n divides a * b & not p |^ n divides a & not p |^ n divides b ) ; :: thesis: contradiction
p divides p |^ n by A3, NEWTON02:6;
then A5: p divides a * b by A4, NAT_D:4;
A6: p > 1 by INT_2:def 4;

per cases ( ( p divides a & p divides b ) or ( not p divides a & p divides b ) or ( p divides a & not p divides b ) or ( not p divides a & not p divides b ) ) ;

suppose ( p divides a & p divides b ) ; :: thesis: contradiction

then p divides 1 by A4, NAT_D:def 5;
hence contradiction by INT_2:27, INT_2:def 4; :: thesis: verum

end;

suppose ( not p divides a & p divides b ) ; :: thesis: contradiction

then p |-count a = 0 by A6, NAT_3:27;
then p |-count (a * b) = 0 + (p |-count b) by A1, A2, NAT_3:28;
then n <= p |-count b by A1, A2, A4, MOEBIUS2:40;
hence contradiction by A2, A4, MOEBIUS1:9; :: thesis: verum

end;

suppose ( p divides a & not p divides b ) ; :: thesis: contradiction

then p |-count b = 0 by A6, NAT_3:27;
then p |-count (a * b) = 0 + (p |-count a) by A1, A2, NAT_3:28;
then n <= p |-count a by A1, A2, A4, MOEBIUS2:40;
hence contradiction by A1, A4, MOEBIUS1:9; :: thesis: verum

end;

suppose ( not p divides a & not p divides b ) ; :: thesis: contradiction

then ( p |-count a = 0 & p |-count b = 0 ) by A6, NAT_3:27;
then p |-count (a * b) = 0 + 0 by A1, A2, NAT_3:28;
hence contradiction by A1, A2, A5, A6, NAT_3:27; :: thesis: verum

end;

end;

end;

end;