let m1, m2, m3, a, b, c be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_coprime & m1,m3 are_coprime & m2,m3 are_coprime 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 that
A1: ( m1 <> 0 & m2 <> 0 ) and
A2: m3 <> 0 and
A3: m1,m2 are_coprime and
A4: ( m1,m3 are_coprime & m2,m3 are_coprime ) ; :: 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 )
consider r being Integer such that
A5: 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 and
A6: ((m1 * r) - (b - a)) mod m2 = 0 by A1, A3, Th40;
m1 * m2 <> 0 by A1, XCMPLX_1:6;
then consider s being Integer such that
A7: ( ( 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 A2, A4, Th40, INT_2:26;
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 that
A8: ( (x - a) mod m1 = 0 & (x - b) mod m2 = 0 ) and
A9: (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 )
x,a + (m1 * r) are_congruent_mod m1 * m2 by A5, A8;
then m1 * m2 divides x - (a + (m1 * r)) ;
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 A6, A7, A9; :: 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