theorem Th76: :: NEWTON02:174

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