let a, b, c be Integer; :: thesis: ( a,b,c are_mutually_distinct implies { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } is infinite )
set A = { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } ;
assume A1: a,b,c are_mutually_distinct ; :: thesis: { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } is infinite
set S = the Sierp45FS of a,b,c;
set r = numberR (a,b,c);
set r0 = numberR0 (a,b,c);
consider h being Integer, F being FinSequence of NAT such that
A2: h = ((a - b) * (a - c)) * (b - c) and
A3: F = Sgm (PrimeDivisors>3 h) and
A4: len the Sierp45FS of a,b,c = len F and
for i being object st i in dom the Sierp45FS of a,b,c holds
( not F . i divides a + ( the Sierp45FS of a,b,c . i) & not F . i divides b + ( the Sierp45FS of a,b,c . i) & not F . i divides c + ( the Sierp45FS of a,b,c . i) ) by A1, Def12;
set X = PrimeDivisors>3 h;
set m = <*2,3*> ^ F;
set u = <*(numberR (a,b,c)),(numberR0 (a,b,c))*> ^ the Sierp45FS of a,b,c;
reconsider u = <*(numberR (a,b,c)),(numberR0 (a,b,c))*> ^ the Sierp45FS of a,b,c as integer-valued FinSequence ;
len <*(numberR (a,b,c)),(numberR0 (a,b,c))*> = 2 by FINSEQ_1:44;
then A5: dom u = Seg (2 + (len the Sierp45FS of a,b,c)) by FINSEQ_1:def 7;
len <*2,3*> = 2 by FINSEQ_1:44;
then A6: dom (<*2,3*> ^ F) = Seg (2 + (len F)) by FINSEQ_1:def 7;
A7: (<*2,3*> ^ F) . 1 = 2 by Th21;
A8: (<*2,3*> ^ F) . 2 = 3 by Th21;
A9: ( a - b <> 0 & a - c <> 0 & b - c <> 0 ) by A1;
<*2,3*> ^ F is positive-yielding

proof

let n be Nat; :: according to RVSUM_3:def 1 :: thesis: ( not n in dom (<*2,3*> ^ F) or not (<*2,3*> ^ F) . n <= 0 )
assume n in dom (<*2,3*> ^ F) ; :: thesis: not (<*2,3*> ^ F) . n <= 0
then A10: (<*2,3*> ^ F) . n in rng (<*2,3*> ^ F) by FUNCT_1:def 3;
rng (<*2,3*> ^ F) c= SetPrimes by A2, A3, A9, Th44;
then (<*2,3*> ^ F) . n is prime by A10, NEWTON:def 6;
hence not (<*2,3*> ^ F) . n <= 0 ; :: thesis: verum

end;

then reconsider m = <*2,3*> ^ F as CR_Sequence by A2, A3, A9, Th45;
set Z = { z where z is positive Nat : z solves_CRT u,m } ;
{ z where z is positive Nat : z solves_CRT u,m } c= { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime }

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { z where z is positive Nat : z solves_CRT u,m } or s in { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } )
assume s in { z where z is positive Nat : z solves_CRT u,m } ; :: thesis: s in { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime }
then consider z being positive Nat such that
A11: s = z and
A12: z solves_CRT u,m ;
u . 1 = numberR (a,b,c) by Th21;
then A13: z, numberR (a,b,c) are_congruent_mod 2 by A7, A12, Th20;
u . 2 = numberR0 (a,b,c) by Th21;
then A14: z, numberR0 (a,b,c) are_congruent_mod 3 by A8, A12, Th20;
for i being Nat st i in dom the Sierp45FS of a,b,c holds
z, the Sierp45FS of a,b,c . i are_congruent_mod F . i

proof

let i be Nat; :: thesis: ( i in dom the Sierp45FS of a,b,c implies z, the Sierp45FS of a,b,c . i are_congruent_mod F . i )
assume A15: i in dom the Sierp45FS of a,b,c ; :: thesis: z, the Sierp45FS of a,b,c . i are_congruent_mod F . i
then A16: z,u . (i + 2) are_congruent_mod m . (i + 2) by A12, Th22;
dom F = dom the Sierp45FS of a,b,c by A4, FINSEQ_3:29;
then m . (i + 2) = F . i by A15, Th23;
hence z, the Sierp45FS of a,b,c . i are_congruent_mod F . i by A15, A16, Th23; :: thesis: verum

end;

then a + z,b + z,c + z are_mutually_coprime by A1, A2, A3, A13, A14, Th43;
hence s in { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } by A11; :: thesis: verum

end;

hence { n where n is positive Nat : a + n,b + n,c + n are_mutually_coprime } is infinite by A4, A5, A6, Th31; :: thesis: verum