theorem Th49: :: NUMBER03:49
for k, n being Nat
for p being odd Prime st n = (p - 1) * ((k * p) + 1) holds
(2 |^ n) mod p = 1