let n be non zero Nat; :: thesis: ( n > 1 implies (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is composite )
assume A1: n > 1 ; :: thesis: (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is composite
set m = ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1;
(1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) >= (1 / 3) * 7 by Th39, XREAL_1:64;
hence (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) >= 2 by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is prime
A2: 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by Th45;
3 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by Th44;
then 7 * 3 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by A2, PEPIN:4, INT_2:30, XPRIMES1:3, XPRIMES1:7;
then consider k being Nat such that
A3: ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 = (7 * 3) * k ;

now :: thesis: not k < 2

assume k < 2 ; :: thesis: contradiction

per cases then ( k = 0 or k = 1 ) by NAT_1:23;

suppose k = 0 ; :: thesis: contradiction

hence contradiction by A3; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A1, A3, Th41; :: thesis: verum

end;

end;

end;

then 7 * k is composite by NUMBER10:3;
hence not (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is prime by A3; :: thesis: verum