let n be Nat; :: thesis: ( n > 1 implies (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is composite )
assume A1: n > 1 ; :: thesis: (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is composite
set W = (2 |^ ((4 * n) + 2)) + 1;
set L = ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1;
set R = ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1;
A2: (2 |^ ((2 * n) + 1)) * (2 |^ ((2 * n) + 1)) = 2 |^ (((2 * n) + 1) + ((2 * n) + 1)) by NEWTON:8;
A3: 2 * (2 |^ ((2 * n) + 1)) = 2 |^ (((2 * n) + 1) + 1) by NEWTON:6;
A4: (2 |^ (n + 1)) * (2 |^ (n + 1)) = 2 |^ ((n + 1) + (n + 1)) by NEWTON:8;
2 |^ (((2 * n) + 1) + 1) = 2 |^ ((n + 1) + (n + 1)) ;
then A5: 2 |^ ((4 * n) + 2) = (((2 |^ ((2 * n) + 1)) * (2 |^ ((2 * n) + 1))) + (2 * (2 |^ ((2 * n) + 1)))) - ((2 |^ (n + 1)) * (2 |^ (n + 1))) by A2, A3, A4;
A6: 2 |^ ((n + 1) + n) = (2 |^ (n + 1)) * (2 |^ n) by NEWTON:8;
A7: n >= 1 + 1 by A1, NAT_1:13;
then n + 1 >= 2 + 1 by XREAL_1:6;
then A8: 2 |^ (n + 1) >= 2 |^ 3 by PREPOWER:93;
A9: 2 |^ n >= 2 |^ 2 by A7, PREPOWER:93;
then (2 |^ n) - 1 >= 4 - 1 by Lm1, XREAL_1:9;
then A10: (2 |^ (n + 1)) * ((2 |^ n) - 1) >= 8 * 3 by A8, Lm2, XREAL_1:66;
then A11: ((2 |^ (n + 1)) * ((2 |^ n) - 1)) + 1 >= 24 + 1 by XREAL_1:6;
then (((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1) * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) >= 25 * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) by A6, XREAL_1:64;
then A12: (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) >= (1 / 5) * (25 * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1)) by A5, XREAL_1:64;
reconsider L = ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 as Element of NAT by A6, A11;
(2 |^ n) + 1 >= 4 + 1 by A9, Lm1, XREAL_1:6;
then A13: (2 |^ (n + 1)) * ((2 |^ n) + 1) >= 8 * 5 by A8, Lm2, XREAL_1:66;
then A14: ((2 |^ (n + 1)) * ((2 |^ n) + 1)) + 1 >= 40 + 1 by XREAL_1:6;
then 5 * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) >= 5 * 41 by A6, XREAL_1:64;
then 2 <= 5 * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) by XXREAL_0:2;
hence 2 <= (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) by A12, XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime
A15: (2 |^ ((4 * n) + 2)) + 1 = L * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) by A5;

per cases then ( 5 divides L or 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 ) by Th40, XPRIMES1:5, INT_5:7;

suppose 5 divides L ; :: thesis: not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime

then consider N being Nat such that
A16: L = 5 * N ;
A17: (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) = (1 / 5) * ((5 * N) * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1)) by A15, A16
.= N * (((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1) ;

A18: now :: thesis: ( N < 2 implies not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime )

assume N < 2 ; :: thesis: not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime
then ( N = 0 or N = 1 ) by NAT_1:23;
hence not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime by A6, A10, A16; :: thesis: verum

end;

((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 >= 2 by A6, A14, XXREAL_0:2;
hence not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime by A17, A18, Th3; :: thesis: verum

end;

suppose 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 ; :: thesis: not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime

then consider N being Nat such that
A19: ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 = 5 * N ;
A20: (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) = (1 / 5) * ((5 * N) * L) by A15, A19
.= N * L ;

A21: now :: thesis: ( N < 2 implies not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime )

assume N < 2 ; :: thesis: not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime
then ( N = 0 or N = 1 ) by NAT_1:23;
hence not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime by A6, A13, A19; :: thesis: verum

end;

L >= 2 by A6, A11, XXREAL_0:2;
hence not (1 / 5) * ((2 |^ ((4 * n) + 2)) + 1) is prime by A20, A21, Th3; :: thesis: verum

end;

end;