let m1, m2, c1, c2 be Integer; ( m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 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 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 ) )
assume that
A1:
m1 <> 0
and
A2:
m2 <> 0
and
A3:
m1 gcd m2 divides c2 - c1
; 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 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
set d = m1 gcd m2;
set d1 = m1 div (m1 gcd m2);
set d2 = m2 div (m1 gcd m2);
set d3 = (c2 - c1) div (m1 gcd m2);
A4:
m1 div (m1 gcd m2),m2 div (m1 gcd m2) are_coprime
by A1, Lm12;
then consider r being Integer such that
A5:
(((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0
by Th15;
take
r
; ( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
A6:
m1 = (m1 div (m1 gcd m2)) * (m1 gcd m2)
by Lm11, INT_2:21;
A7:
m2 = (m2 div (m1 gcd m2)) * (m1 gcd m2)
by Lm11, INT_2:21;
A8:
m1 gcd m2 <> 0
by A1, INT_2:5;
for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2
proof
let x be
Integer;
( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 implies x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 )
assume that A9:
(x - c1) mod m1 = 0
and A10:
(x - c2) mod m2 = 0
;
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2
set y =
(x - c1) div m1;
A11:
x - c1 =
(((x - c1) div m1) * m1) + ((x - c1) mod m1)
by A1, INT_1:59
.=
((x - c1) div m1) * m1
by A9
;
then
x - ((m1 * r) + c1) = m1 * (((x - c1) div m1) - r)
;
then A12:
m1 divides x - ((m1 * r) + c1)
;
(x - c2) mod m2 =
((m1 * ((x - c1) div m1)) - (c2 - c1)) mod m2
by A11
.=
((((m1 gcd m2) * (m1 div (m1 gcd m2))) * ((x - c1) div m1)) - ((m1 gcd m2) * ((c2 - c1) div (m1 gcd m2)))) mod ((m1 gcd m2) * (m2 div (m1 gcd m2)))
by A3, A6, A7, Lm11
;
then
(m2 div (m1 gcd m2)) * (m1 gcd m2) divides (((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) * (m1 gcd m2)
by A2, A7, A10, Lm10;
then
m2 div (m1 gcd m2) divides ((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))
by A8, Th7;
then A13:
(((m1 div (m1 gcd m2)) * ((x - c1) div m1)) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0
by Lm10;
m2 div (m1 gcd m2) <> 0
by A2, A7;
then
r in Class (
(Cong (m2 div (m1 gcd m2))),
((x - c1) div m1))
by A4, A5, A13, Th26;
then
[((x - c1) div m1),r] in Cong (m2 div (m1 gcd m2))
by EQREL_1:18;
then
(x - c1) div m1,
r are_congruent_mod m2 div (m1 gcd m2)
by Def1;
then
m2 div (m1 gcd m2) divides ((x - c1) div m1) - r
;
then consider w being
Integer such that A14:
((x - c1) div m1) - r = (m2 div (m1 gcd m2)) * w
;
x =
c1 + (((x - c1) div m1) * m1)
by A11
.=
c1 + ((((m2 div (m1 gcd m2)) * w) + r) * m1)
by A14
.=
((m1 * r) + c1) + ((w * (m1 div (m1 gcd m2))) * m2)
by A6, A7
;
then
m2 divides x - ((m1 * r) + c1)
;
then
m1 lcm m2 divides x - ((m1 * r) + c1)
by A12, INT_2:19;
hence
x,
c1 + (m1 * r) are_congruent_mod m1 lcm m2
;
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 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
by A5; verum