let x, p be Prime; :: thesis: for k being non zero Nat holds
( x divides p |^ k iff x = p )
let k be non zero Nat; :: thesis: ( x divides p |^ k iff x = p )

A1: now :: thesis: ( x divides p |^ k implies x = p )

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

proof

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

end;

A4: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( x divides p |^ (k + 1) implies x = p )

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

per cases ( x,p are_coprime or x = p ) by INT_2:30;

suppose x,p are_coprime ; :: thesis: x = p

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

end;

suppose x = p ; :: thesis: x = p

hence x = p ; :: thesis: verum

end;

end;

end;

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

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: verum

end;

now :: thesis: ( x = p implies x divides p |^ k )

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

end;

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