let i, n, p be Nat; :: thesis: ( p > 1 & i mod p = 1 implies (i |^ n) mod p = 1 )
assume that
A1: p > 1 and
A2: i mod p = 1 ; :: thesis: (i |^ n) mod p = 1
defpred S₁[ Nat] means (i |^ $1) mod p = 1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: (i |^ k) mod p = 1 ; :: thesis: S₁[k + 1]
(i |^ (k + 1)) mod p = ((i |^ k) * i) mod p by NEWTON:6
.= (((i |^ k) mod p) * i) mod p by EULER_2:8
.= 1 by A2, A4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

1 mod p = 1 by A1, NAT_D:24;
then A5: S₁[ 0 ] by NEWTON:4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A3);
hence (i |^ n) mod p = 1 ; :: thesis: verum