let n be Nat; :: thesis: 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1

per cases ( n = 0 or n > 0 ) ;

suppose A1: n = 0 ; :: thesis: 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1

((2 |^ (2 |^ (0 + 1))) + (2 |^ (2 |^ 0))) + 1 = ((2 |^ 2) + (2 |^ 1)) + 1 by NEWTON:4
.= 7 by Lm2 ;
hence 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by A1; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1

set m = ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1;
A3: 1 mod 7 = 1 by NAT_D:24;
8 = 1 + (7 * 1) ;
then A4: 8 mod 7 = 1 mod 7 by NAT_D:61;
2 |^ (n + 1) = (2 |^ n) * (2 |^ 1) by NEWTON:8;
then A5: 2 |^ (2 |^ (n + 1)) = (2 |^ (2 |^ n)) |^ 2 by NEWTON:9
.= (2 |^ (2 |^ n)) * (2 |^ (2 |^ n)) by WSIERP_1:1 ;

now :: thesis: (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 7 = 0

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 7 = 0

then (2 |^ n) mod 3 = 1 by Th42;
then consider k being Integer such that
A6: 2 |^ n = (k * 3) + 1 by Lm8, NAT_D:64, NAT_6:9;

now :: thesis: not k < 0

assume k < 0 ; :: thesis: contradiction
then (3 * k) + 1 < 0 + 1 by XREAL_1:6;
hence contradiction by A6, NAT_1:14; :: thesis: verum

end;

then reconsider k = k as Element of NAT by INT_1:3;
A7: 1 mod 7 = 1 by NAT_D:24;
A8: 2 |^ (2 |^ n) = (2 |^ (3 * k)) * (2 |^ 1) by A6, NEWTON:8
.= (8 |^ k) * 2 by Lm3, NEWTON:9 ;
A9: (8 |^ k) mod 7 = ((8 mod 7) |^ k) mod 7 by GR_CY_3:30
.= 1 by A3, A4 ;
A10: ((8 |^ k) * 2) mod 7 = (((8 |^ k) mod 7) * (2 mod 7)) mod 7 by NAT_D:67
.= 2 by A9, NAT_D:24 ;
then (2 |^ (2 |^ (n + 1))) mod 7 = (2 * 2) mod 7 by A5, A8, NAT_D:67
.= 4 by NAT_D:24 ;
hence (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 7 = ((4 + 2) + 1) mod 7 by A7, A8, A10, NUMBER05:8
.= 0 ;
:: thesis: verum

end;

suppose n is odd ; :: thesis: (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 7 = 0

then (2 |^ n) mod 3 = 2 by Th43;
then consider k being Integer such that
A11: 2 |^ n = (k * 3) + 2 by Lm9, NAT_D:64, NAT_6:9;

now :: thesis: not k < 0

assume k < 0 ; :: thesis: contradiction
then (3 * k) + 2 < 0 + 2 by XREAL_1:6;
then 2 |^ n = 1 by A11, NAT_1:23
.= 2 |^ 0 by NEWTON:4 ;
hence contradiction by A2; :: thesis: verum

end;

then reconsider k = k as Element of NAT by INT_1:3;
A12: 1 mod 7 = 1 by NAT_D:24;
A13: 2 |^ (2 |^ n) = (2 |^ (3 * k)) * (2 |^ 2) by A11, NEWTON:8
.= (8 |^ k) * 4 by Lm2, Lm3, NEWTON:9 ;
A14: (8 |^ k) mod 7 = ((8 mod 7) |^ k) mod 7 by GR_CY_3:30
.= 1 by A3, A4 ;
A15: ((8 |^ k) * 4) mod 7 = (((8 |^ k) mod 7) * (4 mod 7)) mod 7 by NAT_D:67
.= 4 by A14, NAT_D:24 ;
then (2 |^ (2 |^ (n + 1))) mod 7 = (4 * 4) mod 7 by A5, A13, NAT_D:67
.= (2 + (7 * 2)) mod 7
.= 2 mod 7 by NAT_D:61
.= 2 by NAT_D:24 ;
hence (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 7 = ((4 + 2) + 1) mod 7 by A12, A13, A15, NUMBER05:8
.= 0 ;
:: thesis: verum

end;

end;

end;

hence 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by INT_1:62; :: thesis: verum

end;

end;