theorem :: NEWTON02:140

for k being Nat
for n being odd Prime st n = (2 * k) + 1 holds
( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 )