let a be Nat; :: thesis: for z being non zero Nat holds 3 divides (2 |^ (2 |^ z)) + ((6 * a) - 1)
let z be non zero Nat; :: thesis: 3 divides (2 |^ (2 |^ z)) + ((6 * a) - 1)
A1: (3 * (2 * a)) mod 3 = 0 by NAT_D:13;
A2: ((6 * a) - 1) mod 3 = (((6 * a) mod 3) - (1 mod 3)) mod 3 by INT_6:7
.= (0 - 1) mod 3 by A1, NAT_D:24
.= (- 1) mod 3
.= 2 by Th9 ;
((2 |^ (2 |^ z)) + ((6 * a) - 1)) mod 3 = (((2 |^ (2 |^ z)) mod 3) + (((6 * a) - 1) mod 3)) mod 3 by NAT_D:66
.= (1 + 2) mod 3 by A2, Th39
.= 0 by NAT_D:25 ;
hence 3 divides (2 |^ (2 |^ z)) + ((6 * a) - 1) by INT_1:62; :: thesis: verum