set P1 = ((2 |^ 32) - 1) * 641;
set P2 = 6700417;
set P3 = 2;
set PPP = <*(((2 |^ 32) - 1) * 641),6700417,2*>;
A1: for i, j being Nat st i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i < j holds
<*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

proof

let i, j be Nat; :: thesis: ( i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i < j implies <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime )
assume A2: ( i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i < j ) ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime
A3: ( 1 <= i & j <= len <*(((2 |^ 32) - 1) * 641),6700417,2*> & len <*(((2 |^ 32) - 1) * 641),6700417,2*> = 2 + 1 ) by A2, FINSEQ_1:45, FINSEQ_3:25;

per cases then ( j = 2 + 1 or j <= 2 ) by NAT_1:9;

suppose A4: j = 2 + 1 ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

A5: (320 * 2) + 1 is odd ;
(2 |^ 32) - 1 = (2 |^ 32) -' 1 by NAT_1:14, XREAL_1:233;
then consider j being Nat such that
A6: ((2 |^ 32) -' 1) * 641 = (2 * j) + 1 by A5, ABIAN:9;
2,1 are_coprime ;
then A7: ( 2,(2 * 3350208) + 1 are_coprime & 2,(2 * j) + 1 are_coprime ) by NUMBER04:64;
i <= 1 + 1 by A4, A2, NAT_1:13;

per cases then ( i = 2 or i <= 1 ) by NAT_1:9;

suppose i = 2 ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

hence <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime by A7, A4; :: thesis: verum

end;

suppose i <= 1 ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

then i = 1 by A3, XXREAL_0:1;
hence <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime by NAT_1:14, XREAL_1:233, A4, A7, A6; :: thesis: verum

end;

end;

end;

suppose A8: j <= 2 ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

then i < 1 + 1 by A2, XXREAL_0:2;
then i <= 1 by NAT_1:13;
then A9: i = 1 by A3, XXREAL_0:1;
1 < j by A2, A3, XXREAL_0:2;
then 1 + 1 <= j by NAT_1:13;
then j = 2 by A8, XXREAL_0:1;
hence <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime by A9, Th29; :: thesis: verum

end;

end;

end;

A10: for i, j being Nat st i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i <> j holds
<*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime

proof

let i, j be Nat; :: thesis: ( i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i <> j implies <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime )
assume A11: ( i in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & j in dom <*(((2 |^ 32) - 1) * 641),6700417,2*> & i <> j ) ; :: thesis: <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime
( i < j or j < i ) by A11, XXREAL_0:1;
hence <*(((2 |^ 32) - 1) * 641),6700417,2*> . i,<*(((2 |^ 32) - 1) * 641),6700417,2*> . j are_coprime by A1, A11; :: thesis: verum

end;

reconsider PPP = <*(((2 |^ 32) - 1) * 641),6700417,2*> as INT -valued non empty positive-yielding Chinese_Remainder FinSequence by A10, INT_6:def 2;
( 1 in INT & - 1 in INT & 2 in INT ) by INT_1:def 2;
then reconsider B = <*1,(- 1),1*> as FinSequence of INT by FINSEQ_2:14;
take crt = CRT (B,PPP); :: thesis: ( 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 ) ) )
(((2 |^ 32) - 1) * 641) * 6700417 = ((2 |^ 32) - 1) * (641 * 6700417)
.= ((2 |^ 32) - 1) * ((2 |^ 32) + 1) by Th28
.= ((2 |^ 32) * (2 |^ 32)) - (1 * 1)
.= (2 |^ (32 + 32)) - 1 by NEWTON:8 ;
then A12: Product PPP = 2 * ((2 |^ 64) - 1) by RVSUM_1:100;
A13: ( len B = 3 & 3 = len PPP ) by FINSEQ_1:45;
then A14: dom B = dom PPP by FINSEQ_3:29;
A15: ( crt solves_CRT B,PPP & crt < Product PPP ) by A14, NUMBER14:def 4;
A16: 2 in dom B by A13, FINSEQ_3:25;
A17: 3 in dom B by A13, FINSEQ_3:25;
thus 6700417 < crt :: thesis: ( 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 ) ) )

proof

A18: crt,B . 2 are_congruent_mod PPP . 2 by A15, A16, NUMBER14:def 3;
A19: ( crt,B . 3 are_congruent_mod PPP . 3 & B . 3 = 1 ) by A17, A15, NUMBER14:def 3;
assume 6700417 >= crt ; :: thesis: contradiction

per cases then ( 6700417 = crt or 6700417 > crt ) by XXREAL_0:1;

suppose 6700417 = crt ; :: thesis: contradiction

then 0 ,crt are_congruent_mod 6700417 by INT_1:12;
then 0 , - 1 are_congruent_mod 6700417 by A18, INT_1:15;
hence contradiction by INT_2:13; :: thesis: verum

end;

suppose A20: 6700417 > crt ; :: thesis: contradiction

0 ,6700417 are_congruent_mod 6700417 by INT_1:12;
then crt + 0,6700417 + (- 1) are_congruent_mod 6700417 by A18, INT_1:16;
then ( crt mod 6700417 = 6700416 mod 6700417 & 6700416 mod 6700417 = 6700416 ) by NAT_D:24, NAT_D:64;
then 2 divides 6700416 - 1 by A19, NAT_D:24, A20;
then 2 divides (3350207 * 2) + 1 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

thus crt < 2 * ((2 |^ 64) - 1) by A14, NUMBER14:def 4, A12; :: thesis: 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 )
let n be Nat; :: thesis: ( 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 )
1 in dom B by A13, FINSEQ_3:25;
then crt + (n * (Product PPP)),B . 1 are_congruent_mod PPP . 1 by A14, A15, NUMBER14:30, NUMBER14:def 3;
hence crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 by A12; :: thesis: ( crt + ((n * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 & crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2 )
crt + (n * (Product PPP)),B . 2 are_congruent_mod PPP . 2 by A14, A15, NUMBER14:30, NUMBER14:def 3, A16;
hence crt + ((n * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 by A12; :: thesis: crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2
( crt + (n * (Product PPP)),B . 3 are_congruent_mod PPP . 3 & B . 3 = 1 ) by A17, A14, A15, NUMBER14:30, NUMBER14:def 3;
hence crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2 by A12; :: thesis: verum