let p, i, n be Nat; :: thesis: ( p is prime & i divides p |^ n & not i = 1 implies ex k being Element of NAT st i = p * k )
assume A1: p is prime ; :: thesis: ( not i divides p |^ n or i = 1 or ex k being Element of NAT st i = p * k )
then A2: p <> 0 by INT_2:def 5;
defpred S₁[ Nat] means ( not i divides p |^ $1 or i = 1 or ex k being Element of NAT st i = p * k );
A3: S₁[ 0 ]

proof

now

assume i divides p |^ 0 ; :: thesis: S₁[ 0 ]
then i divides 1 by NEWTON:9;
then consider t being Nat such that
A4: 1 = i * t by NAT_D:def 3;
thus S₁[ 0 ] by A4, NAT_1:15; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]

now

assume i divides p |^ (n + 1) ; :: thesis: S₁[n + 1]
then consider u1 being Nat such that
A7: p |^ (n + 1) = i * u1 by NAT_D:def 3;
p * (p |^ n) = i * u1 by A7, NEWTON:11;
then A8: p divides i * u1 by NAT_D:def 3;

now

per cases ( p divides i or p divides u1 ) by A1, A8, NEWTON:98;

suppose p divides i ; :: thesis: S₁[n + 1]

then consider w1 being Nat such that
A9: i = p * w1 by NAT_D:def 3;
w1 in NAT by ORDINAL1:def 13;
hence S₁[n + 1] by A9; :: thesis: verum

end;

suppose p divides u1 ; :: thesis: S₁[n + 1]

then consider w2 being Nat such that
A10: u1 = p * w2 by NAT_D:def 3;
p * (p |^ n) = p * (i * w2) by A7, A10, NEWTON:11;
then p |^ n = (p * (i * w2)) div p by A2, NAT_D:18;
then p |^ n = i * w2 by A2, NAT_D:18;
then consider w3 being Element of NAT such that
A11: ( i = p * w3 or i = 1 ) by A6, NAT_D:def 3;
thus S₁[n + 1] by A11; :: thesis: verum

end;

end;

end;

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

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A5);
hence ( not i divides p |^ n or i = 1 or ex k being Element of NAT st i = p * k ) ; :: thesis: verum