let a be Integer; :: thesis: for x, n being Nat holds (a |^ x) mod n = ((a mod n) |^ x) mod n
let x, n be Nat; :: thesis: (a |^ x) mod n = ((a mod n) |^ x) mod n
defpred S₁[ Nat] means (a |^ $1) mod n = ((a mod n) |^ $1) mod n;
A1: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
A2: (a |^ (x + 1)) mod n = ((a |^ x) * a) mod n by NEWTON:6
.= (((a |^ x) mod n) * (a mod n)) mod n by NAT_D:67 ;
A3: ((a mod n) |^ (x + 1)) mod n = (((a mod n) |^ x) * (a mod n)) mod n by NEWTON:6
.= ((((a mod n) |^ x) mod n) * ((a mod n) mod n)) mod n by NAT_D:67
.= ((((a mod n) |^ x) mod n) * (a mod n)) mod n by NAT_D:65 ;
assume (a |^ x) mod n = ((a mod n) |^ x) mod n ; :: thesis: S₁[x + 1]
hence S₁[x + 1] by A2, A3; :: thesis: verum

end;

a |^ 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, A1);
hence (a |^ x) mod n = ((a mod n) |^ x) mod n ; :: thesis: verum