theorem Th77: :: NEWTON02:175

for a, n being Nat holds 7 divides (a |^ ((6 * n) + 1)) - a