let a be Nat; :: thesis: for n being positive Nat holds 3 divides (((3 * a) + 2) * (2 |^ (2 |^ n))) + 1
let n be positive Nat; :: thesis: 3 divides (((3 * a) + 2) * (2 |^ (2 |^ n))) + 1
A1: 3 divides (2 * (2 |^ (2 |^ n))) + 1 by Lm13;
A2: 3 divides 3 * (a * (2 |^ (2 |^ n))) ;
(((3 * a) + 2) * (2 |^ (2 |^ n))) + 1 = ((3 * a) * (2 |^ (2 |^ n))) + ((2 * (2 |^ (2 |^ n))) + 1) ;
hence 3 divides (((3 * a) + 2) * (2 |^ (2 |^ n))) + 1 by A1, A2, NAT_D:8; :: thesis: verum