let m1, m2, c1, c2 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 implies ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) )
assume that
A1: m1 <> 0 and
A2: m2 <> 0 and
A3: m1 gcd m2 divides c2 - c1 ; :: thesis: ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
set d = m1 gcd m2;
set d1 = m1 div (m1 gcd m2);
set d2 = m2 div (m1 gcd m2);
set d3 = (c2 - c1) div (m1 gcd m2);
A4: m1 div (m1 gcd m2),m2 div (m1 gcd m2) are_coprime by A1, Lm12;
then consider r being Integer such that
A5: (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Th15;
take r ; :: thesis: ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
A6: m1 = (m1 div (m1 gcd m2)) * (m1 gcd m2) by Lm11, INT_2:21;
A7: m2 = (m2 div (m1 gcd m2)) * (m1 gcd m2) by Lm11, INT_2:21;
A8: m1 gcd m2 <> 0 by A1, INT_2:5;
for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2

proof

let x be Integer; :: thesis: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 implies x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 )
assume that
A9: (x - c1) mod m1 = 0 and
A10: (x - c2) mod m2 = 0 ; :: thesis: x,c1 + (m1 * r) are_congruent_mod m1 lcm m2
set y = (x - c1) div m1;
A11: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:59
.= ((x - c1) div m1) * m1 by A9 ;
then x - ((m1 * r) + c1) = m1 * (((x - c1) div m1) - r) ;
then A12: m1 divides x - ((m1 * r) + c1) ;
(x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 by A11
.= ((((m1 gcd m2) * (m1 div (m1 gcd m2))) * ((x - c1) div m1)) - ((m1 gcd m2) * ((c2 - c1) div (m1 gcd m2)))) mod ((m1 gcd m2) * (m2 div (m1 gcd m2))) by A3, A6, A7, Lm11 ;
then (m2 div (m1 gcd m2)) * (m1 gcd m2) divides (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) * (m1 gcd m2) by A2, A7, A10, Lm10;
then m2 div (m1 gcd m2) divides ((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2)) by A8, Th7;
then A13: (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 by Lm10;
m2 div (m1 gcd m2) <> 0 by A2, A7;
then r in Class ((Cong (m2 div (m1 gcd m2))),((x - c1) div m1)) by A4, A5, A13, Th26;
then [((x - c1) div m1),r] in Cong (m2 div (m1 gcd m2)) by EQREL_1:18;
then (x - c1) div m1,r are_congruent_mod m2 div (m1 gcd m2) by Def1;
then m2 div (m1 gcd m2) divides ((x - c1) div m1) - r ;
then consider w being Integer such that
A14: ((x - c1) div m1) - r = (m2 div (m1 gcd m2)) * w ;
x = c1 + (((x - c1) div m1) * m1) by A11
.= c1 + ((((m2 div (m1 gcd m2)) * w) + r) * m1) by A14
.= ((m1 * r) + c1) + ((w * (m1 div (m1 gcd m2))) * m2) by A6, A7 ;
then m2 divides x - ((m1 * r) + c1) ;
then m1 lcm m2 divides x - ((m1 * r) + c1) by A12, INT_2:19;
hence x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ; :: thesis: verum

end;

hence ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) by A5; :: thesis: verum