let p be Prime; :: thesis: for m, n being Nat holds
( not m divides n * p or m divides n or ex z being Nat st
( m = z * p & z divides n ) )
let m, n be Nat; :: thesis: ( not m divides n * p or m divides n or ex z being Nat st
( m = z * p & z divides n ) )
assume m divides n * p ; :: thesis: ( m divides n or ex z being Nat st
( m = z * p & z divides n ) )
then consider a, b being Nat such that
A1: a divides n and
A2: b divides p and
A3: m = a * b by NUMBER12:14;
assume A4: not m divides n ; :: thesis: ex z being Nat st
( m = z * p & z divides n )

per cases ( b = 1 or b = p ) by A2, INT_2:def 4;

suppose b = 1 ; :: thesis: ex z being Nat st
( m = z * p & z divides n )

hence ex z being Nat st
( m = z * p & z divides n ) by A1, A3, A4; :: thesis: verum

end;

suppose A5: b = p ; :: thesis: ex z being Nat st
( m = z * p & z divides n )

take a ; :: thesis: ( m = a * p & a divides n )
thus m = a * p by A3, A5; :: thesis: a divides n
thus a divides n by A1; :: thesis: verum

end;

end;