let m, n be non zero Element of NAT ; :: thesis: ( m divides n & not m is square-containing implies m divides Radical n )
assume A1: ( m divides n & not m is square-containing ) ; :: 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)
A2: p > 1 by INT_2:def 5;

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

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

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

end;

end;

end;

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