set X = { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ;
set n = (28 * 1) + 1;
(((2 |^ (2 * ((28 * 1) + 1))) + 1) |^ 2) + (2 |^ 2) is composite by Th78;
then A1: (((2 |^ (2 * ((28 * 1) + 1))) + 1) |^ 2) + (2 |^ 2) in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ;
A2: { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } or not x is natural )
assume x in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ; :: thesis: x is natural
then ex n being Nat st
( x = (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) & (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite ) ;
hence x is natural ; :: thesis: verum

end;

for a being Nat st a in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } holds
ex b being Nat st
( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )

proof

let a be Nat; :: thesis: ( a in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } implies ex b being Nat st
( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ) )
assume a in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ; :: thesis: ex b being Nat st
( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )
then consider n being Nat such that
A3: a = (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) and
(((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite ;

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

suppose A4: n <> 0 ; :: thesis: ex b being Nat st
( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )

take b = (((2 |^ (2 * ((28 * n) + 1))) + 1) |^ 2) + (2 |^ 2); :: thesis: ( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )
A5: ((2 |^ (2 * n)) + 1) |^ 2 = ((2 |^ (2 * n)) + 1) ^2 by WSIERP_1:1;
A6: ((2 |^ (2 * ((28 * n) + 1))) + 1) |^ 2 = ((2 |^ (2 * ((28 * n) + 1))) + 1) ^2 by WSIERP_1:1;
A7: 1 * n <= 28 * n by XREAL_1:64;
(28 * n) + 0 < (28 * n) + 1 by XREAL_1:8;
then n < (28 * n) + 1 by A7, XXREAL_0:2;
then 2 * n < 2 * ((28 * n) + 1) by XREAL_1:68;
then 2 |^ (2 * n) < 2 |^ (2 * ((28 * n) + 1)) by PEPIN:66;
then (2 |^ (2 * n)) + 1 < (2 |^ (2 * ((28 * n) + 1))) + 1 by XREAL_1:8;
then ((2 |^ (2 * n)) + 1) ^2 < ((2 |^ (2 * ((28 * n) + 1))) + 1) ^2 by XREAL_1:96;
hence b > a by A3, A5, A6, XREAL_1:8; :: thesis: b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite }
b is composite by A4, Th78;
hence b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ex b being Nat st
( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )

then A8: a = ((1 + 1) |^ 2) + 4 by A3, Lm1, NEWTON:4
.= 4 + 4 by Lm1 ;
set z = (28 * 1) + 1;
take b = (((2 |^ (2 * ((28 * 1) + 1))) + 1) |^ 2) + (2 |^ 2); :: thesis: ( b > a & b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } )
A9: 2 |^ 0 = 1 by NEWTON:4;
2 |^ (2 * ((28 * 1) + 1)) > 2 |^ 0 by PEPIN:66;
then (2 |^ (2 * ((28 * 1) + 1))) + 1 > 1 + 1 by A9, XREAL_1:8;
then ((2 |^ (2 * ((28 * 1) + 1))) + 1) |^ 2 > 2 |^ 2 by PREPOWER:10;
hence b > a by A8, Lm1, XREAL_1:8; :: thesis: b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite }
b is composite by Th78;
hence b in { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } ; :: thesis: verum

end;

end;

end;

hence { ((((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)) where n is Nat : (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite } is infinite by A1, A2, NUMBER04:1; :: thesis: verum