let n be Nat; :: thesis:
let p be Prime; :: thesis:
assume A1: for r being Nat holds n <> p |^ r ; :: thesis:

per cases ;

suppose A2: n = 0 ; :: thesis:

per cases ;

suppose A3: p = 2 ; :: thesis:

take s = 3; :: thesis:
thus s is prime by PEPIN:41; :: thesis:
thus s divides n by A2, INT_2:12; :: thesis:
thus s <> p by A3; :: thesis:

end;

suppose A4: p <> 2 ; :: thesis:

take s = 2; :: thesis:
thus s is prime by INT_2:28; :: thesis:
thus s divides n by A2, INT_2:12; :: thesis:
thus s <> p by A4; :: thesis:

end;

end;

end;

suppose A5: n <> 0 ; :: thesis:

A6: p > 1 by INT_2:def 4;
reconsider r1 = p |-count n as Element of NAT ;
A7: p |^ r1 divides n by A5, A6, NAT_3:def 7;
A8: not p |^ (r1 + 1) divides n by A5, A6, NAT_3:def 7;
consider s1 being Nat such that
A9: n = (p |^ r1) * s1 by A7, NAT_D:def 3;
s1 >= 2

proof

assume not s1 >= 2 ; :: thesis:
then s1 < 1 + 1 ;
then s1 <= 1 by NAT_1:13;
then ( s1 = 0 or s1 = 1 ) by NAT_1:25;
hence contradiction by A5, A1, A9; :: thesis:

end;

then consider s being Element of NAT such that
A10: s is prime and
A11: s divides s1 by INT_2:31;
A12: s1 divides n by A9, NAT_D:def 3;
take s ; :: thesis:
s <> p

proof

assume s = p ; :: thesis:
then consider s2 being Nat such that
A13: s1 = p * s2 by A11, NAT_D:def 3;
n = ((p |^ r1) * p) * s2 by A9, A13
.= (p |^ (r1 + 1)) * s2 by NEWTON:6 ;
hence contradiction by A8, NAT_D:def 3; :: thesis:

end;

hence ( s is prime & s divides n & s <> p ) by A10, A11, A12, NAT_D:4; :: thesis:

end;

end;