let k be Integer; :: thesis: ( k <> 1 implies { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite )
assume A1: k <> 1 ; :: thesis: { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite
set X = { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ;
A2: not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty by A1, Lm13;
A3: { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is natural-membered

proof

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

end;

for w being Nat st w in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } holds
ex b being Nat st
( b > w & b in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } )

proof

let w be Nat; :: thesis: ( w in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } implies ex b being Nat st
( b > w & b in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ) )
assume w in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ; :: thesis: ex b being Nat st
( b > w & b in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } )
consider n being positive Nat such that
A4: w < (2 |^ (2 |^ n)) + k and
A5: (2 |^ (2 |^ n)) + k is composite by A1, Th70;
reconsider b = (2 |^ (2 |^ n)) + k as positive Nat by A4;
take b ; :: thesis: ( b > w & b in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } )
thus ( b > w & b in { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } ) by A4, A5; :: thesis: verum

end;

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