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