let p be natural prime number ; :: thesis: for x being Element of (Z/Z* p)
for i being integer number
for n being natural number st x = i holds
x |^ n = (i |^ n) mod p

let x be Element of (Z/Z* p); :: thesis: for i being integer number
for n being natural number st x = i holds
x |^ n = (i |^ n) mod p

let i be integer number ; :: thesis: for n being natural number st x = i holds
x |^ n = (i |^ n) mod p

let n be natural number ; :: 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(# (),() #) by INT_7:def 4;
Segm0 p = (Segm p) \ by ;
then A3: i in Segm p by ;
reconsider i = i as Element of NAT by ;
defpred S1[ 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 ;
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: S1[ 0 ] by ;
A8: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[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
.= ((i |^ k) * i) mod p by NAT_D:67
.= (i |^ (k + 1)) mod p by NEWTON:6 ;
hence S1[k + 1] ; :: thesis: verum
end;
A10: for k being Nat holds S1[k] from NAT_1:sch 2(A7, A8);
thus x |^ n = (i |^ n) mod p by A10; :: thesis: verum