let n be positive Nat; :: thesis: 3 divides (2 * (2 |^ (2 |^ n))) + 1
2 |^ ((n - 1) + 1) = 2 * (2 |^ (n - 1)) by NEWTON:6;
then 2 + 1 divides (2 |^ ((2 |^ n) + 1)) + (1 |^ ((2 |^ n) + 1)) by NEWTON01:35;
hence 3 divides (2 * (2 |^ (2 |^ n))) + 1 by NEWTON:6; :: thesis: verum