let n be Nat; (2 |^ (2 |^ n)) + 1 divides (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2
set A = 2 |^ (2 |^ n);
set F = (2 |^ (2 |^ n)) + 1;
set G = (2 |^ (2 |^ (n + 1))) - 1;
set H = (2 |^ (2 |^ (2 |^ n))) - 1;
set I = 2 |^ ((2 |^ (2 |^ n)) + 1);
n + 1 <= 2 |^ n
by NEWTON:85;
then A1:
(2 |^ (2 |^ (n + 1))) - 1 divides (2 |^ (2 |^ (2 |^ n))) - 1
by Th19, NEWTON:89;
((2 |^ (2 |^ n)) + 1) * ((2 |^ (2 |^ n)) - 1) =
((2 |^ (2 |^ n)) |^ 2) - (1 |^ 2)
by NEWTON01:1
.=
(2 |^ ((2 |^ n) * (2 |^ 1))) - 1
by NEWTON:9
.=
(2 |^ (2 |^ (n + 1))) - 1
by NEWTON:8
;
then
(2 |^ (2 |^ n)) + 1 divides (2 |^ (2 |^ (n + 1))) - 1
;
then A2:
(2 |^ (2 |^ n)) + 1 divides (2 |^ (2 |^ (2 |^ n))) - 1
by A1, INT_2:9;
(2 |^ 1) * (2 |^ (2 |^ (2 |^ n))) = 2 |^ ((2 |^ (2 |^ n)) + 1)
by NEWTON:8;
then
2 * ((2 |^ (2 |^ (2 |^ n))) - 1) = (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2
;
then
(2 |^ (2 |^ (2 |^ n))) - 1 divides (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2
;
hence
(2 |^ (2 |^ n)) + 1 divides (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2
by A2, INT_2:9; verum