let k, n be Nat; ( n = (28 * k) + 1 implies 29 divides (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) )
assume A1:
n = (28 * k) + 1
; 29 divides (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)
set x = (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2);
A2:
Euler 29 = 29 - 1
by EULER_1:20, XPRIMES1:29;
A3:
(2 |^ 28) |^ (2 * k) = 2 |^ (28 * (2 * k))
by NEWTON:9;
(2 |^ (Euler 29)) mod 29 = 1
by EULER_2:18, XPRIMES1:2, XPRIMES1:29, INT_2:30;
then
2 |^ 28,1 are_congruent_mod 29
by A2, PEPIN:39;
then
(2 |^ 28) |^ (2 * k),1 |^ (2 * k) are_congruent_mod 29
by GR_CY_3:34;
then A4:
(2 |^ (2 * (28 * k))) * 4,1 * 4 are_congruent_mod 29
by A3, INT_4:11;
2 |^ (2 * ((28 * k) + 1)) =
2 |^ ((2 * (28 * k)) + 2)
.=
(2 |^ (2 * (28 * k))) * (2 |^ 2)
by NEWTON:8
;
then
(2 |^ (2 * n)) + 1,4 + 1 are_congruent_mod 29
by A1, A4, Lm1;
then
((2 |^ (2 * n)) + 1) |^ 2,5 |^ 2 are_congruent_mod 29
by GR_CY_3:34;
then
(((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2),29 are_congruent_mod 29
by Lm1, Lm2;
then ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) mod 29 =
29 mod 29
by NAT_D:64
.=
0
by NAT_D:25
;
hence
29 divides (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)
by INT_1:62; verum