let n be Nat; :: thesis: for p being Prime st n is perfect_power & p divides n holds
p |^ 2 divides n
let p be Prime; :: thesis: ( n is perfect_power & p divides n implies p |^ 2 divides n )
assume A0: ( n is perfect_power & p divides n ) ; :: thesis: p |^ 2 divides n
then consider x, k being Nat such that
A1: ( k > 1 & n = x |^ k ) by NUMBER06:def 10;
A2: 1 + 1 <= k by A1, NAT_1:13;
A3: p |^ k divides x |^ k by NEWTON03:15, A1, A0, NAT_3:5;
p |^ 2 divides p |^ k by A2, NEWTON:89;
hence p |^ 2 divides n by A1, A3, NAT_D:4; :: thesis: verum