let p be natural prime number ; 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); 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 ; for n being natural number st x = i holds
x |^ n = (i |^ n) mod p
let n be natural number ; ( x = i implies x |^ n = (i |^ n) mod p )
assume A1:
x = i
; 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 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 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:
S1[ 0 ]
by A4, A6, INT_7:21;
A8:
now for k being Nat st S1[k] holds
S1[k + 1]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; verum