theorem :: NUMBER03:46

for n being Nat holds
( not 1 < n or not n divides (2 |^ n) - 1 )