let p be Prime; :: thesis: for m being Nat st m is square-free & p divides m holds
{ d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
let m be Nat; :: thesis: ( m is square-free & p divides m implies { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) } )
assume that
A1: m is square-free and
A2: p divides m ; :: thesis: { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }
set B = { d where d is Element of NAT : ( 0 < d & d divides m div p ) } ;
set A = { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } ;
thus { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } c= { d where d is Element of NAT : ( 0 < d & d divides m div p ) } :: according to XBOOLE_0:def 10 :: thesis: { d where d is Element of NAT : ( 0 < d & d divides m div p ) } c= { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } or x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } )
assume x in { d where d is Element of NAT : ( 0 < d & d divides m div p ) } ; :: thesis: x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) }
then consider d being Element of NAT such that
A5: ( d = x & 0 < d ) and
A6: d divides m div p ;
( d divides m & not p divides d ) by A1, A2, A6, Th27;
hence x in { d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } by A5; :: thesis: verum