let n be Nat; :: thesis: for i, j, m being Integer st i mod m = j mod m holds
(i |^ n) mod m = (j |^ n) mod m
let i, j, m be Integer; :: thesis: ( i mod m = j mod m implies (i |^ n) mod m = (j |^ n) mod m )
defpred S₁[ Nat] means (i |^ $1) mod m = (j |^ $1) mod m;
assume A1: i mod m = j mod m ; :: thesis: (i |^ n) mod m = (j |^ n) mod m
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus (i |^ (n + 1)) mod m = ((i |^ n) * i) mod m by NEWTON:6
.= (((j |^ n) mod m) * (j mod m)) mod m by A1, A3, NAT_D:67
.= ((j |^ n) * j) mod m by NAT_D:67
.= (j |^ (n + 1)) mod m by NEWTON:6 ; :: thesis: verum

end;

i |^ 0 = 1 by NEWTON:4;
then A4: S₁[ 0 ] by NEWTON:4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2);
hence (i |^ n) mod m = (j |^ n) mod m ; :: thesis: verum