let m1, m2, m3, a, b, c be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_relative_prime & m1,m3 are_relative_prime & m2,m3 are_relative_prime implies ex r, s being Integer st
for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) )
assume A1: ( m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_relative_prime & m1,m3 are_relative_prime & m2,m3 are_relative_prime ) ; :: thesis: ex r, s being Integer st
for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )
then consider r being Integer such that
A2: ( ( for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 holds
x,a + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (b - a)) mod m2 = 0 ) by Th40;
A3: m1 * m2 <> 0 by A1, XCMPLX_1:6;
m1 * m2,m3 are_relative_prime by A1, INT_2:41;
then consider s being Integer such that
A4: ( ( for x being Integer st (x - (a + (m1 * r))) mod (m1 * m2) = 0 & (x - c) mod m3 = 0 holds
x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 ) & (((m1 * m2) * s) - (c - (a + (m1 * r)))) mod m3 = 0 ) by A1, A3, Th40;
take r ; :: thesis: ex s being Integer st
for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )
take s ; :: thesis: for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )
for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )

proof

let x be Integer; :: thesis: ( (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 implies ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) )
assume A5: ( (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 ) ; :: thesis: ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )
then x,a + (m1 * r) are_congruent_mod m1 * m2 by A2;
then m1 * m2 divides x - (a + (m1 * r)) by INT_2:19;
then (x - (a + (m1 * r))) mod (m1 * m2) = 0 by Lm10;
hence ( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) by A2, A4, A5; :: thesis: verum

end;

hence for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 ) ; :: thesis: verum