let a, b, m be Nat; :: thesis: for p being Prime st m <> 0 & p |^ m divides a * b & not p divides a holds
p divides b
let p be Prime; :: thesis: ( m <> 0 & p |^ m divides a * b & not p divides a implies p divides b )
assume that
A1: m <> 0 and
A2: p |^ m divides a * b ; :: thesis: ( p divides a or p divides b )
p divides p |^ m by A1, NAT_3:3;
then p divides a * b by A2, INT_2:9;
hence ( p divides a or p divides b ) by INT_5:7; :: thesis: verum