let p be Prime; :: thesis: for n, a, b being Nat st p divides a & not p divides b & n = a / b holds
p divides n
let n, a, b be Nat; :: thesis: ( p divides a & not p divides b & n = a / b implies p divides n )
assume that
A0: ( p divides a & not p divides b ) and
B2: n = a / b ; :: thesis: p divides n

per cases ( not b is zero or b is zero ) ;

suppose B1: not b is zero ; :: thesis: p divides n

consider x being Nat such that
A1: p * x = a by A0, NAT_D:def 3;
A2: p * (x / b) = (p * x) / b ;
consider u being Nat such that
A3: b * u = p * x by B2, A1, Lm3b, B1, NAT_D:def 3;
p divides u by A0, A3, NAT_D:def 3, NEWTON:80;
then consider v being Nat such that
A4: p * v = u by NAT_D:def 3;
( (b * v) * p = x * p & p <> 0 ) by A3, A4;
then b divides x by XCMPLX_1:5, NAT_D:def 3;
then x / b is Nat by B1, Lm3b;
hence p divides n by B2, A1, A2, NAT_D:def 3; :: thesis: verum

end;

suppose b is zero ; :: thesis: p divides n

then n = 0 by B2;
hence p divides n by INT_2:12; :: thesis: verum

end;

end;