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