let a be Nat; :: thesis: for z being non zero Nat st 1 <= a holds
(2 |^ (2 |^ z)) + ((6 * a) - 1) is composite
let z be non zero Nat; :: thesis: ( 1 <= a implies (2 |^ (2 |^ z)) + ((6 * a) - 1) is composite )
assume A1: 1 <= a ; :: thesis: (2 |^ (2 |^ z)) + ((6 * a) - 1) is composite
then 6 < (2 |^ (2 |^ z)) + ((6 * a) - 1) by Th61;
hence 2 <= (2 |^ (2 |^ z)) + ((6 * a) - 1) by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime
thus not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime by A1, Th63; :: thesis: verum