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

( 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