let i, n, p be Nat; :: thesis: ( p is prime & i divides p |^ n & not i = 1 implies ex k being Element of NAT st i = p * k )
defpred S₁[ Nat] means ( not i divides p |^ $1 or i = 1 or 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 4;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

now :: thesis: ( i divides p |^ (n + 1) implies S₁[n + 1] )

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

now :: thesis: S₁[n + 1]

per cases ( p divides i or p divides u1 ) by A1, A6, NEWTON:80;

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

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

end;

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

then consider w2 being Nat such that
A8: u1 = p * w2 by NAT_D:def 3;
p * (p |^ n) = p * (i * w2) by A5, A8, NEWTON:6;
then p |^ n = (p * (i * w2)) div p by A2, NAT_D:18;
then p |^ n = i * w2 by A2, NAT_D:18;
hence S₁[n + 1] by A4, NAT_D:def 3; :: thesis: verum

end;

end;

end;

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

end;

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

end;

A9: S₁[ 0 ]

proof

now :: thesis: ( i divides p |^ 0 implies S₁[ 0 ] )

assume i divides p |^ 0 ; :: thesis: S₁[ 0 ]
then i divides 1 by NEWTON:4;
then ex t being Nat st 1 = i * t by NAT_D:def 3;
hence S₁[ 0 ] by NAT_1:15; :: thesis: verum

end;

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

end;

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