let a, b, m be Nat; :: thesis: for n being Element of NAT st a mod m = b mod m holds

(a |^ n) mod m = (b |^ n) mod m

let n be Element of NAT ; :: thesis: ( a mod m = b mod m implies (a |^ n) mod m = (b |^ n) mod m )

defpred S_{1}[ Nat] means (a |^ $1) mod m = (b |^ $1) mod m;

assume A1: a mod m = b mod m ; :: thesis: (a |^ n) mod m = (b |^ n) mod m

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A4: S_{1}[ 0 ]
by NEWTON:4;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2);

hence (a |^ n) mod m = (b |^ n) mod m ; :: thesis: verum

(a |^ n) mod m = (b |^ n) mod m

let n be Element of NAT ; :: thesis: ( a mod m = b mod m implies (a |^ n) mod m = (b |^ n) mod m )

defpred S

assume A1: a mod m = b mod m ; :: thesis: (a |^ n) mod m = (b |^ n) mod m

A2: for k being Nat st S

S

proof

a |^ 0 = 1
by NEWTON:4;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider l1 = a |^ k, l2 = b |^ k, a = a, b = b, m = m as Element of NAT by ORDINAL1:def 12;

(a |^ (k + 1)) mod m = ((a |^ k) * a) mod m by NEWTON:6

.= ((l1 mod m) * (a mod m)) mod m by EULER_2:9

.= (l2 * b) mod m by A1, A3, EULER_2:9

.= (b |^ (k + 1)) mod m by NEWTON:6 ;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

reconsider l1 = a |^ k, l2 = b |^ k, a = a, b = b, m = m as Element of NAT by ORDINAL1:def 12;

(a |^ (k + 1)) mod m = ((a |^ k) * a) mod m by NEWTON:6

.= ((l1 mod m) * (a mod m)) mod m by EULER_2:9

.= (l2 * b) mod m by A1, A3, EULER_2:9

.= (b |^ (k + 1)) mod m by NEWTON:6 ;

hence S

then A4: S

for k being Nat holds S

hence (a |^ n) mod m = (b |^ n) mod m ; :: thesis: verum