let a, c, k, m, n, t2 be Nat; ( 2 |^ k,a are_congruent_mod n & (((a * a) * a) * a) * (2 |^ m) = (n * t2) + c implies 2 |^ ((k * 4) + m),c are_congruent_mod n )
assume that
A1:
2 |^ k,a are_congruent_mod n
and
A2:
(((a * a) * a) * a) * (2 |^ m) = (n * t2) + c
; 2 |^ ((k * 4) + m),c are_congruent_mod n
A3:
(((a * a) * a) * a) * (2 |^ m),c are_congruent_mod n
by A2;
A4: ((2 |^ k) * (2 |^ k)) * ((2 |^ k) * (2 |^ k)) =
(((2 |^ k) * (2 |^ k)) * (2 |^ k)) * (2 |^ k)
.=
(2 |^ k) |^ 4
by POLYEQ_5:3
;
(2 |^ k) * (2 |^ k),a * a are_congruent_mod n
by A1, INT_1:18;
then
((2 |^ k) * (2 |^ k)) * ((2 |^ k) * (2 |^ k)),(a * a) * (a * a) are_congruent_mod n
by INT_1:18;
then
( (2 |^ k) |^ 4,((a * a) * a) * a are_congruent_mod n & 2 |^ m,2 |^ m are_congruent_mod n )
by A4, INT_1:11;
then
((2 |^ k) |^ 4) * (2 |^ m),(((a * a) * a) * a) * (2 |^ m) are_congruent_mod n
by INT_1:18;
then A:
((2 |^ k) |^ 4) * (2 |^ m),c are_congruent_mod n
by A3, INT_1:15;
2 |^ ((k * 4) + m) = (2 |^ (k * 4)) * (2 |^ m)
by NEWTON:8;
hence
2 |^ ((k * 4) + m),c are_congruent_mod n
by A, NEWTON:9; verum