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(# (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_{1}[ 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_{1}[ 0 ]
by A4, A6, INT_7:21;

_{1}[k]
from NAT_1:sch 2(A7, A8);

thus x |^ n = (i |^ n) mod p by A10; :: thesis: verum

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(# (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

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

A8: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A10:
for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A9: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
; :: thesis: verum

end;assume A9: S

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

thus x |^ n = (i |^ n) mod p by A10; :: thesis: verum