let s be positive Nat; 11 divides (2 |^ (2 |^ ((4 * s) + 1))) + 7
A1:
2 * (2 |^ (4 * s)) = 2 |^ ((4 * s) + 1)
by NEWTON:6;
5 divides (2 |^ (4 * s)) - 1
by Th31;
then
2 * 5 divides 2 * ((2 |^ (4 * s)) - 1)
by INT_4:7;
then consider k being Integer such that
A2:
(2 |^ ((4 * s) + 1)) - 2 = 10 * k
by A1;
k >= 0
by A2;
then reconsider k = k as Element of NAT by INT_1:3;
A3: 2 |^ (2 |^ ((4 * s) + 1)) =
2 |^ ((10 * k) + 2)
by A2
.=
(2 |^ (10 * k)) * (2 |^ 2)
by NEWTON:8
.=
((2 |^ 10) |^ k) * (2 |^ 2)
by NEWTON:9
;
2 |^ 10 =
((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:6
.=
(93 * 11) + 1
;
then
2 |^ 10,1 are_congruent_mod 11
;
then
(2 |^ 10) |^ k,1 |^ k are_congruent_mod 11
by GR_CY_3:34;
then
((2 |^ 10) |^ k) * 4,1 * 4 are_congruent_mod 11
by INT_4:11;
then
(((2 |^ 10) |^ k) * 4) + 7,4 + 7 are_congruent_mod 11
;
then
(((2 |^ 10) |^ k) * 4) + 7, 0 are_congruent_mod 11
by Th27;
hence
11 divides (2 |^ (2 |^ ((4 * s) + 1))) + 7
by A3, Lm1; verum