let p, q be Prime; :: thesis: for n, m being Nat st p divides m * (q |^ n) & p <> q holds
p divides m
let n, m be Nat; :: thesis: ( p divides m * (q |^ n) & p <> q implies p divides m )
assume that
A1: p divides m * (q |^ n) and
A2: p <> q ; :: thesis: p divides m
( p divides m or p divides q |^ n ) by A1, NEWTON:80;
hence p divides m by A2, NAT_3:6; :: thesis: verum