theorem Th30: :: NUMBER19:30

for k being Nat st k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k > 6700417 holds
for n being positive Nat holds
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )