let x, p be natural prime number ; :: thesis:
let k be natural non zero number ; :: thesis:

A1: now :: thesis:

assume A2: x divides p |^ k ; :: thesis:
defpred S₁[ Nat] means ( x divides p |^ $1 implies x = p );
A3: S₁[1]

proof

assume x divides p |^ 1 ; :: thesis:
then x divides p ;
then ( x = 1 or x = p ) by INT_2:def 4;
hence x = p by NAT_2:def 1; :: thesis:

end;

A4: now :: thesis:

let k be non zero Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:

now :: thesis:

assume A6: x divides p |^ (k + 1) ; :: thesis:
A7: p |^ (k + 1) = p * (p |^ k) by NEWTON:6;

per cases by INT_2:30;

suppose x,p are_coprime ; :: thesis:

hence x = p by A5, A6, A7, INT_2:25; :: thesis:

end;

suppose x = p ; :: thesis:

hence x = p ; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

A8: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A3, A4);
thus x = p by A8, A2; :: thesis:

end;

now :: thesis:

assume A9: x = p ; :: thesis:
reconsider k1 = k - 1 as natural number ;
p * (p |^ k1) = p |^ (k1 + 1) by NEWTON:6;
hence x divides p |^ k by A9; :: thesis:

end;

hence ( x divides p |^ k iff x = p ) by A1; :: thesis: