theorem Th31: :: NUMBER19:31

ex crt being Nat st
( 6700417 < crt & crt < 2 * ((2 |^ 64) - 1) & ( for n being Nat holds
( crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 & crt + ((n * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 & crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2 ) ) )