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