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

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