let a be Nat; :: thesis: for z being non zero Nat st 1 <= a holds
not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime
let z be non zero Nat; :: thesis: ( 1 <= a implies not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime )
set p = (2 |^ (2 |^ z)) + ((6 * a) - 1);
assume A1: 1 <= a ; :: thesis: not (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime
assume (2 |^ (2 |^ z)) + ((6 * a) - 1) is prime ; :: thesis: contradiction
then 3 = (2 |^ (2 |^ z)) + ((6 * a) - 1) by Th62;
hence contradiction by A1, Th61; :: thesis: verum