let m, n be non zero Nat; :: thesis: ( m divides n & m is square-free implies m divides Radical n )
assume that
A1: m divides n and
A2: m is square-free ; :: thesis: m divides Radical n
for p being Prime holds p |-count m <= p |-count (Radical n)

proof

let p be Prime; :: thesis: p |-count m <= p |-count (Radical n)
A3: p > 1 by INT_2:def 4;

per cases ( p divides m or not p divides m ) ;

suppose p divides m ; :: thesis: p |-count m <= p |-count (Radical n)

then p divides n by A1, NAT_D:4;
then p divides Radical n by Th56;
then A4: p |-count (Radical n) <> 0 by A3, NAT_3:27;
p |-count (Radical n) <= 1 by Th61;
then A5: p |-count (Radical n) < 1 + 1 by NAT_1:13;
p |-count m <= 1 by A2, Th24;
hence p |-count m <= p |-count (Radical n) by A5, A4, NAT_1:23; :: thesis: verum

end;

suppose not p divides m ; :: thesis: p |-count m <= p |-count (Radical n)

hence p |-count m <= p |-count (Radical n) by A3, NAT_3:27; :: thesis: verum

end;

end;

end;

hence m divides Radical n by Th19; :: thesis: verum