let n be Nat; :: thesis: 3 divides (2 |^ (2 * n)) - 1
4 - 1 divides (4 |^ n) - 1 by GR_CY_3:27;
hence 3 divides (2 |^ (2 * n)) - 1 by Lm1, NEWTON:9; :: thesis: verum