let a, m, i be Nat; :: thesis: for A being sequence of NAT st A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) holds
A . i = (a to_power (2 to_power i)) mod m
let A be sequence of NAT; :: thesis: ( A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) implies A . i = (a to_power (2 to_power i)) mod m )
assume AS0: ( A . 0 = a mod m & ( for i being Nat holds A . (i + 1) = ((A . i) * (A . i)) mod m ) ) ; :: thesis: A . i = (a to_power (2 to_power i)) mod m
defpred S1[ Nat] means A . $1 = (a to_power (2 to_power $1)) mod m;
(a to_power (2 to_power 0)) mod m = (a to_power 1) mod m by POWER:24
.= a mod m ;
then L1: S1[ 0 ] by AS0;
L2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; :: thesis: S1[i + 1]
then ((A . i) * (A . i)) mod m = (a |^ ((2 to_power 1) * (2 to_power i))) mod m by NAT_4:11
.= (a to_power (2 to_power (i + 1))) mod m by POWER:27 ;
hence S1[i + 1] by AS0; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(L1, L2);
 hence A . i = (a to_power (2 to_power i)) mod m ; :: thesis: verum