theorem Th56: :: NEWTON02:154

for a being Nat
for n being prime Nat holds n * a divides ((a + 1) |^ n) - ((a |^ n) + 1)