let p be Prime; :: thesis: for m, d being Nat st m is square-free & p divides m & d divides m div p holds
( d divides m & not p divides d )
let m, d be Nat; :: thesis: ( m is square-free & p divides m & d divides m div p implies ( d divides m & not p divides d ) )
assume that
A1: m is square-free and
A2: p divides m ; :: thesis: ( not d divides m div p or ( d divides m & not p divides d ) )
assume d divides m div p ; :: thesis: ( d divides m & not p divides d )
then consider z being Nat such that
A3: m div p = d * z by NAT_D:def 3;
A4: (m div p) * p = (d * z) * p by A3;
then m = d * (z * p) by A2, NAT_D:3;
hence d divides m by NAT_D:def 3; :: thesis: not p divides d
assume p divides d ; :: thesis: contradiction
then consider w being Nat such that
A5: d = p * w by NAT_D:def 3;
m = (w * (p * p)) * z by A2, A4, A5, NAT_D:3
.= (w * (p |^ 2)) * z by WSIERP_1:1
.= (p |^ 2) * (w * z) ;
then p |^ 2 divides m by NAT_D:def 3;
hence contradiction by A1; :: thesis: verum