theorem Th56: :: PEPIN:56

for n, p being Nat st p is prime & p > 2 & p divides Fermat n holds
ex k being Element of NAT st p = (k * (2 |^ (n + 1))) + 1