let m1, m2, a, b, c1, c2 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_coprime implies ex w, r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) )
assume that
A1: m1 <> 0 and
A2: m2 <> 0 and
A3: a gcd m1 divides c1 and
A4: b gcd m2 divides c2 and
A5: m1,m2 are_coprime ; :: thesis: ex w, r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
set d2 = b gcd m2;
A6: b gcd m2 <> 0 by A2, INT_2:5;
set d1 = a gcd m1;
A7: a gcd m1 <> 0 by A1, INT_2:5;
A8: a div (a gcd m1),m1 div (a gcd m1) are_coprime by A1, Lm12;
then consider r being Integer such that
A9: (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 by Th15;
A10: c2 = (c2 div (b gcd m2)) * (b gcd m2) by A4, Lm11;
A11: b = (b div (b gcd m2)) * (b gcd m2) by Lm11, INT_2:21;
A12: m2 = (m2 div (b gcd m2)) * (b gcd m2) by Lm11, INT_2:21;
then A13: m2 div (b gcd m2) divides m2 ;
A14: m2 div (b gcd m2) <> 0 by A2, A12;
A15: c1 = (c1 div (a gcd m1)) * (a gcd m1) by A3, Lm11;
A16: a = (a div (a gcd m1)) * (a gcd m1) by Lm11, INT_2:21;
A17: b div (b gcd m2),m2 div (b gcd m2) are_coprime by A2, Lm12;
then consider s being Integer such that
A18: (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 by Th15;
A19: m1 = (m1 div (a gcd m1)) * (a gcd m1) by Lm11, INT_2:21;
then A20: m1 div (a gcd m1) divides m1 ;
A21: m1 div (a gcd m1),m2 div (b gcd m2) are_coprime

proof

reconsider e = (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) as Element of NAT by ORDINAL1:def 12;
assume not m1 div (a gcd m1),m2 div (b gcd m2) are_coprime ; :: thesis: contradiction
then A22: (m1 div (a gcd m1)) gcd (m2 div (b gcd m2)) <> 1 by INT_2:def 3;
e divides m2 div (b gcd m2) by INT_2:21;
then A23: e divides m2 by A13, INT_2:9;
e divides m1 div (a gcd m1) by INT_2:21;
then e divides m1 by A20, INT_2:9;
then e divides m1 gcd m2 by A23, INT_2:22;
then e divides 1 by A5, INT_2:def 3;
hence contradiction by A22, WSIERP_1:15; :: thesis: verum

end;

then consider w being Integer such that
A24: (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 by Th15;
take w ; :: thesis: ex r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
take r ; :: thesis: ex s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
take s ; :: thesis: ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
A25: m1 div (a gcd m1) <> 0 by A1, A19;
for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2))

proof

let x be Integer; :: thesis: ( ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 implies x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) )
assume that
A26: ((a * x) - c1) mod m1 = 0 and
A27: ((b * x) - c2) mod m2 = 0 ; :: thesis: x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2))
(m1 div (a gcd m1)) * (a gcd m1) divides (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) * (a gcd m1) by A1, A19, A15, A16, A26, Lm10;
then m1 div (a gcd m1) divides ((a div (a gcd m1)) * x) - (c1 div (a gcd m1)) by A7, Th7;
then (((a div (a gcd m1)) * x) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 by Lm10;
then r in Class ((Cong (m1 div (a gcd m1))),x) by A8, A9, A25, Th26;
then [x,r] in Cong (m1 div (a gcd m1)) by EQREL_1:18;
then x,r are_congruent_mod m1 div (a gcd m1) by Def1;
then A28: m1 div (a gcd m1) divides x - r ;
(m2 div (b gcd m2)) * (b gcd m2) divides (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) * (b gcd m2) by A2, A12, A10, A11, A27, Lm10;
then m2 div (b gcd m2) divides ((b div (b gcd m2)) * x) - (c2 div (b gcd m2)) by A6, Th7;
then (((b div (b gcd m2)) * x) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 by Lm10;
then s in Class ((Cong (m2 div (b gcd m2))),x) by A17, A18, A14, Th26;
then [x,s] in Cong (m2 div (b gcd m2)) by EQREL_1:18;
then x,s are_congruent_mod m2 div (b gcd m2) by Def1;
then A29: m2 div (b gcd m2) divides x - s ;
m2 div (b gcd m2) divides ((m1 div (a gcd m1)) * w) - (s - r) by A14, A24, Lm10;
then A30: m2 div (b gcd m2) divides (x - s) - ((((m1 div (a gcd m1)) * w) + r) - s) by A29, Lm4;
m1 div (a gcd m1) divides (m1 div (a gcd m1)) * w ;
then m1 div (a gcd m1) divides (x - r) - ((m1 div (a gcd m1)) * w) by A28, Lm4;
then (m1 div (a gcd m1)) * (m2 div (b gcd m2)) divides x - (r + ((m1 div (a gcd m1)) * w)) by A21, A30, Lm13;
hence x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ; :: thesis: verum

end;

hence ( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 ) by A9, A18, A24; :: thesis: verum