let p be Prime; :: thesis: not p is perfect_power
A0: p > 1 by INT_2:def 4;
assume p is perfect_power ; :: thesis: contradiction
then consider x, k being Nat such that
A1: ( k > 1 & p = x |^ k ) ;
x |^ 1 = x ;

per cases then ( x = 1 or x = p ) by A1, INT_2:def 4, NEWTON:89;

suppose x = 1 ; :: thesis: contradiction

hence contradiction by A1, INT_2:def 4; :: thesis: verum

end;

suppose x = p ; :: thesis: contradiction

then p |^ 1 = p |^ k by A1;
hence contradiction by A1, A0, PEPIN:30; :: thesis: verum

end;

end;