let k be Integer; :: thesis: ( k <> 1 implies { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite )
assume A1: k <> 1 ; :: thesis: { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite
then { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } , { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } are_equipotent by Th71;
hence { n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite by A1, Th72, CARD_1:38; :: thesis: verum