theorem :: NUMBER14:56
for m being non zero Nat ex s being Nat st
for n being Nat st n > s holds
((2 |^ m) * (2 |^ (2 |^ n))) + 1 is composite