let p be Prime; :: thesis: for m, d being Nat st p divides m & d divides m & not p divides d holds
d divides m div p
let m, d be Nat; :: thesis: ( p divides m & d divides m & not p divides d implies d divides m div p )
assume that
A1: p divides m and
A2: d divides m and
A3: not p divides d ; :: thesis: d divides m div p
consider z being Nat such that
A4: m = d * z by A2, NAT_D:def 3;
p divides z by A1, A3, A4, NEWTON:80;
then consider u being Nat such that
A5: z = p * u by NAT_D:def 3;
m = (d * u) * p by A4, A5;
then m div p = d * u by NAT_D:18;
hence d divides m div p by NAT_D:def 3; :: thesis: verum