theorem Th40: :: NEWTON02:138

for n being prime Nat holds n divides (2 |^ n) - 2