let a, m, i, n be Nat; :: thesis: for A being sequence of NAT st a <> 0 & A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) holds
(((a to_power n) mod m) * (A . i)) mod m = (a to_power (n + (2 to_power i))) mod m
let A be sequence of NAT; :: thesis: ( a <> 0 & A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) implies (((a to_power n) mod m) * (A . i)) mod m = (a to_power (n + (2 to_power i))) mod m )
assume AS0: ( a <> 0 & A . 0 = a mod m & ( for i being Nat holds A . (i + 1) = ((A . i) * (A . i)) mod m ) ) ; :: thesis: (((a to_power n) mod m) * (A . i)) mod m = (a to_power (n + (2 to_power i))) mod m
then A . i = (a to_power (2 to_power i)) mod m by CBPOW1;
then (((a to_power n) mod m) * (A . i)) mod m = ((a to_power n) * (a to_power (2 to_power i))) mod m by NAT_D:67
.= (a to_power (n + (2 to_power i))) mod m by POWER:27, AS0 ;
hence (((a to_power n) mod m) * (A . i)) mod m = (a to_power (n + (2 to_power i))) mod m ; :: thesis: verum