let m1, m2, m3, a, b, c be Integer; ( 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 )
; 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
; 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
; 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 )
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 )
; verum