let s be positive Nat; 37 divides (2 |^ (2 |^ ((6 * s) + 2))) + 21
A1:
(2 |^ 2) * (2 |^ (6 * s)) = 2 |^ (2 + (6 * s))
by NEWTON:8;
9 divides (2 |^ (6 * s)) - 1
by Th34;
then
4 * 9 divides 4 * ((2 |^ (6 * s)) - 1)
by INT_4:7;
then consider k being Integer such that
A2:
(2 |^ ((6 * s) + 2)) - 4 = 36 * k
by A1, Lm1;
k >= 0
by A2, Lm1;
then reconsider k = k as Element of NAT by INT_1:3;
A3: 2 |^ (2 |^ ((6 * s) + 2)) =
2 |^ ((36 * k) + 4)
by A2
.=
(2 |^ (36 * k)) * (2 |^ 4)
by NEWTON:8
.=
((2 |^ 36) |^ k) * (2 |^ 4)
by NEWTON:9
;
2 |^ (18 + 18) =
(2 |^ 18) * (2 |^ 18)
by NEWTON:8
.=
(1857283155 * 37) + 1
by Lm10
;
then
2 |^ 36,1 are_congruent_mod 37
;
then
(2 |^ 36) |^ k,1 |^ k are_congruent_mod 37
by GR_CY_3:34;
then
((2 |^ 36) |^ k) * 16,1 * 16 are_congruent_mod 37
by INT_4:11;
then
(((2 |^ 36) |^ k) * 16) + 21,16 + 21 are_congruent_mod 37
;
then
(((2 |^ 36) |^ k) * 16) + 21, 0 are_congruent_mod 37
by Th27;
hence
37 divides (2 |^ (2 |^ ((6 * s) + 2))) + 21
by A3, Lm3; verum