let p be Prime; :: thesis: for x being Element of (Z/Z* p)
for i being Integer
for n being Nat st x = i holds
x |^ n = (i |^ n) mod p
let x be Element of (Z/Z* p); :: thesis: for i being Integer
for n being Nat st x = i holds
x |^ n = (i |^ n) mod p
let i be Integer; :: thesis: for n being Nat st x = i holds
x |^ n = (i |^ n) mod p
let n be Nat; :: thesis: ( x = i implies x |^ n = (i |^ n) mod p )
assume A1: x = i ; :: thesis: x |^ n = (i |^ n) mod p
A2: Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #) by INT_7:def 4;
Segm0 p = (Segm p) \ {0} by INT_2:def 4, INT_7:def 2;
then A3: i in Segm p by A2, A1, XBOOLE_0:def 5;
reconsider i = i as Element of NAT by A1, A2, INT_1:3;
defpred S₁[ Nat] means x |^ $1 = (i |^ $1) mod p;
A4: x |^ 0 = 1_ (Z/Z* p) by GROUP_1:25;
1 < p by INT_2:def 4;
then A5: 1 div p <= 1 - 1 by INT_1:56, INT_1:52;
A6: 1 div p = 0 by A5;
i |^ 0 = 1 by NEWTON:4;
then (i |^ 0) mod p = 1 - ((1 div p) * p) by INT_1:def 10;
then A7: S₁[ 0 ] by A4, A6, INT_7:21;

A8: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
x |^ (k + 1) = (x |^ k) * x by GROUP_1:34
.= (((i |^ k) mod p) * i) mod p by A1, A9, Th16
.= (((i |^ k) mod p) * (i mod p)) mod p by A3, NAT_D:24, NAT_1:44
.= ((i |^ k) * i) mod p by NAT_D:67
.= (i |^ (k + 1)) mod p by NEWTON:6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
thus x |^ n = (i |^ n) mod p by A10; :: thesis: verum