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