let m, n be non zero Element of 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 ) ;
end;
end;
hence m divides Radical n by Th19; :: thesis: verum