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 S₁[ 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: S₁[ 0 ] by AS0;
L2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[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 S₁[i + 1] by AS0; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(L1, L2);
hence A . i = (a to_power (2 to_power i)) mod m ; :: thesis: verum