let n be Nat; :: thesis: 5 divides (2 |^ ((4 * n) + 2)) + 1
A1: (2 |^ 2) + 1 divides ((2 |^ 2) |^ ((2 * n) + 1)) + (1 |^ ((2 * n) + 1)) by NEWTON01:35;
(2 |^ 2) |^ ((2 * n) + 1) = 2 |^ (2 * ((2 * n) + 1)) by NEWTON:9;
hence 5 divides (2 |^ ((4 * n) + 2)) + 1 by A1, Lm1; :: thesis: verum