let k, n be non zero Nat; :: thesis: ( ( k divides n & k is square-free ) iff k divides Radical n )
A1: ( k divides Radical n implies ( k divides n & k is square-free ) )
proof
assume A2: k divides Radical n ; :: thesis: ( k divides n & k is square-free )
Radical n divides n by Th55;
hence ( k divides n & k is square-free ) by A2, Th26, NAT_D:4; :: thesis: verum
end;
( k is non zero Element of NAT & n is non zero Element of NAT ) by ORDINAL1:def 12;
hence ( ( k divides n & k is square-free ) iff k divides Radical n ) by A1, Lm5; :: thesis: verum