theorem :: NUMBER13:38

for k being positive Nat holds
( ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) iff k in {2,5,8} )