let n be non zero Nat; :: thesis: { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
thus { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } c= { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } c= { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } or x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } ; :: thesis: x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
then consider k1 being Element of NAT such that
A1: k1 = x and
A2: 0 < k1 and
A3: ( k1 divides n & k1 is square-free ) ;
k1 divides Radical n by A2, A3, Th65;
hence x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } by A1, A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } or x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } ; :: thesis: x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) }
then consider k1 being Element of NAT such that
A4: ( x = k1 & 0 < k1 ) and
A5: k1 divides Radical n ;
A6: k1 is square-free by A5, Th26;
Radical n divides n by Th55;
then k1 divides n by A5, NAT_D:4;
hence x in { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } by A4, A6; :: thesis: verum