let s be positive Nat; 29 divides (2 |^ (2 |^ ((6 * s) + 2))) + 13
A1:
(2 |^ 2) * (2 |^ (6 * s)) = 2 |^ (2 + (6 * s))
by NEWTON:8;
7 divides (2 |^ (6 * s)) - 1
by Th32;
then
4 * 7 divides 4 * ((2 |^ (6 * s)) - 1)
by INT_4:7;
then consider k being Integer such that
A2:
(2 |^ ((6 * s) + 2)) - 4 = 28 * 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 |^ ((28 * k) + 4)
by A2
.=
(2 |^ (28 * k)) * (2 |^ 4)
by NEWTON:8
.=
((2 |^ 28) |^ k) * (2 |^ 4)
by NEWTON:9
;
2 |^ (14 + 14) =
(2 |^ 14) * (2 |^ 14)
by NEWTON:8
.=
(9256395 * 29) + 1
by Lm9
;
then
2 |^ 28,1 are_congruent_mod 29
;
then
(2 |^ 28) |^ k,1 |^ k are_congruent_mod 29
by GR_CY_3:34;
then
((2 |^ 28) |^ k) * 16,1 * 16 are_congruent_mod 29
by INT_4:11;
then
(((2 |^ 28) |^ k) * 16) + 13,16 + 13 are_congruent_mod 29
;
then
(((2 |^ 28) |^ k) * 16) + 13, 0 are_congruent_mod 29
by Th27;
hence
29 divides (2 |^ (2 |^ ((6 * s) + 2))) + 13
by A3, Lm3; verum