theorem :: NUMBER19:33

for k being Nat st k = (((15 * 1000000000) * 1000000000) + (511380746 * 1000000000)) + 462593381 holds
( k > 6700417 & k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k,1 are_congruent_mod 2 & not Fermat 0 divides (k * (2 |^ (2 |^ 5))) + 1 & ... & not Fermat 4 divides (k * (2 |^ (2 |^ 5))) + 1 & not 6700417 divides (k * (2 |^ (2 |^ 5))) + 1 & 641 divides (k * (2 |^ (2 |^ 5))) + 1 )