let m1, m2, c1, c2 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & m1,m2 are_coprime 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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) )
assume that
A1: m1 <> 0 and
A2: m2 <> 0 and
A3: m1,m2 are_coprime ; :: 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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 )
consider r being Integer such that
A4: ((m1 * r) - (c2 - c1)) mod m2 = 0 by A3, 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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 )
for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 * 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 * m2 )
assume that
A5: (x - c1) mod m1 = 0 and
A6: (x - c2) mod m2 = 0 ; :: thesis: x,c1 + (m1 * r) are_congruent_mod m1 * m2
set y = (x - c1) div m1;
A7: x - c1 = (((x - c1) div m1) * m1) + ((x - c1) mod m1) by A1, INT_1:59
.= ((x - c1) div m1) * m1 by A5 ;
then (x - c2) mod m2 = ((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2 ;
then (x - c1) div m1 in Class ((Cong m2),r) by A2, A3, A4, A6, Th26;
then [r,((x - c1) div m1)] in Cong m2 by EQREL_1:18;
then r,(x - c1) div m1 are_congruent_mod m2 by Def1;
then (x - c1) div m1,r are_congruent_mod m2 by INT_1:14;
then m2 divides ((x - c1) div m1) - r ;
then consider t being Integer such that
A8: ((x - c1) div m1) - r = m2 * t ;
x = c1 + (((x - c1) div m1) * m1) by A7
.= c1 + ((r + (m2 * t)) * m1) by A8
.= (c1 + (r * m1)) + ((m1 * m2) * t) ;
then m1 * m2 divides x - (c1 + (r * m1)) ;
hence x,c1 + (m1 * r) are_congruent_mod m1 * 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 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 ) by A4; :: thesis: verum