theorem Th41: :: NAT_6:41

for l being 2 _or_greater Nat
for k being positive Nat st not 3 divides k & k <= (2 |^ l) - 1 holds
( (k * (2 |^ l)) + 1 is prime iff 3 |^ (k * (2 |^ (l - 1))), - 1 are_congruent_mod (k * (2 |^ l)) + 1 )