theorem Th77: :: NUMBER07:77

for k, n being Nat st n = (28 * k) + 1 holds
29 divides (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2)