let a, b, c be Integer; :: thesis: for n1, n2, n3 being non zero Nat st n1 gcd n2 divides a - b holds
ex r, s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )
let n1, n2, n3 be non zero Nat; :: thesis: ( n1 gcd n2 divides a - b implies ex r, s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) )
set d1 = n1 gcd n2;
set d2 = n1 gcd n3;
set d3 = n2 gcd n3;
set dd1 = n1 gcd n2;
set K = n1 lcm n2;
A1: n2 divides n1 lcm n2 by NAT_D:def 4;
assume n1 gcd n2 divides a - b ; :: thesis: ex r, s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )
then n1 gcd n2 divides - (a - b) by INT_2:10;
then consider r being Integer such that
A2: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 holds
x,a + (n1 * r) are_congruent_mod n1 lcm n2 and
A3: (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 by Th42;
take r ; :: thesis: ex s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )
set y = a + (n1 * r);
A4: (n1 lcm n2) div ((n1 lcm n2) gcd n3),n3 div ((n1 lcm n2) gcd n3) are_coprime by Lm12;
then consider s being Integer such that
A5: ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 by Th15;
take s ; :: thesis: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )
A6: n1 divides n1 lcm n2 by NAT_D:def 4;
A7: for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
(n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c
proof
let x be Integer; :: thesis: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 implies (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c )
assume that
A8: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 ) and
A9: (x - c) mod n3 = 0 ; :: thesis: (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c
A10: n3 divides x - c by A9, Lm10;
x,a + (n1 * r) are_congruent_mod n1 lcm n2 by A2, A8;
then n1 lcm n2 divides x - (a + (n1 * r)) ;
then A11: n1 lcm n2 divides - (x - (a + (n1 * r))) by INT_2:10;
then n1 divides (a + (n1 * r)) - x by A6, INT_2:9;
then consider t1 being Integer such that
A12: (a + (n1 * r)) - x = n1 * t1 ;
n2 gcd n3 divides n3 by NAT_D:def 5;
then A13: n2 gcd n3 divides x - c by A10, INT_2:9;
n1 gcd n3 divides n3 by NAT_D:def 5;
then A14: n1 gcd n3 divides x - c by A10, INT_2:9;
n2 divides (a + (n1 * r)) - x by A1, A11, INT_2:9;
then consider t2 being Integer such that
A15: (a + (n1 * r)) - x = n2 * t2 ;
n2 gcd n3 divides n2 by NAT_D:def 5;
then A16: n2 gcd n3 divides n2 * t2 by INT_2:2;
(a + (n1 * r)) - c = (x - c) + (n2 * t2) by A15;
then A17: n2 gcd n3 divides (a + (n1 * r)) - c by A16, A13, WSIERP_1:4;
n1 gcd n3 divides n1 by NAT_D:def 5;
then A18: n1 gcd n3 divides n1 * t1 by INT_2:2;
(a + (n1 * r)) - c = (x - c) + (n1 * t1) by A12;
then n1 gcd n3 divides (a + (n1 * r)) - c by A18, A14, WSIERP_1:4;
then (n1 gcd n3) lcm (n2 gcd n3) divides (a + (n1 * r)) - c by A17, INT_2:19;
hence (n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c by Th46; :: thesis: verum
end;
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3
proof
A19: n1 lcm n2 <> 0 by INT_2:4;
let x be Integer; :: thesis: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 implies x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 )
assume that
A20: ( (x - a) mod n1 = 0 & (x - b) mod n2 = 0 ) and
A21: (x - c) mod n3 = 0 ; :: thesis: x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3
(n1 lcm n2) gcd n3 divides (a + (n1 * r)) - c by A7, A20, A21;
then (n1 lcm n2) gcd n3 divides - ((a + (n1 * r)) - c) by INT_2:10;
then consider w being Integer such that
A22: for x being Integer st (x - (a + (n1 * r))) mod (n1 lcm n2) = 0 & (x - c) mod n3 = 0 holds
x,(a + (n1 * r)) + ((n1 lcm n2) * w) are_congruent_mod (n1 lcm n2) lcm n3 and
A23: ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * w) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 by A19, Th42;
A24: n3 = (n3 div ((n1 lcm n2) gcd n3)) * ((n1 lcm n2) gcd n3) by Lm11, INT_2:21;
then n3 div ((n1 lcm n2) gcd n3) <> 0 ;
then w in Class ((Cong (n3 div ((n1 lcm n2) gcd n3))),s) by A4, A5, A23, Th26;
then [s,w] in Cong (n3 div ((n1 lcm n2) gcd n3)) by EQREL_1:18;
then s,w are_congruent_mod n3 div ((n1 lcm n2) gcd n3) by Def1;
then A25: (n1 lcm n2) * s,(n1 lcm n2) * w are_congruent_mod (n1 lcm n2) * (n3 div ((n1 lcm n2) gcd n3)) by Th10;
(n1 lcm n2) * (n3 div ((n1 lcm n2) gcd n3)) = (((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * ((n1 lcm n2) gcd n3)) * (n3 div ((n1 lcm n2) gcd n3)) by Lm11, INT_2:21
.= n3 * ((n1 lcm n2) div ((n1 lcm n2) gcd n3)) by A24 ;
then (n1 lcm n2) * s,(n1 lcm n2) * w are_congruent_mod n3 by A25, INT_1:20;
then A26: n3 divides ((n1 lcm n2) * s) - ((n1 lcm n2) * w) ;
n1 lcm n2 divides (n1 lcm n2) * (s - w) ;
then (n1 lcm n2) lcm n3 divides (((n1 lcm n2) * s) + (a + (n1 * r))) - (((n1 lcm n2) * w) + (a + (n1 * r))) by A26, INT_2:19;
then ((n1 lcm n2) * s) + (a + (n1 * r)),((n1 lcm n2) * w) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 ;
then A27: ((n1 lcm n2) * w) + (a + (n1 * r)),((n1 lcm n2) * s) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 by INT_1:14;
x,a + (n1 * r) are_congruent_mod n1 lcm n2 by A2, A20;
then n1 lcm n2 divides x - (a + (n1 * r)) ;
then (x - (a + (n1 * r))) mod (n1 lcm n2) = 0 by Lm10;
then x,((n1 lcm n2) * w) + (a + (n1 * r)) are_congruent_mod (n1 lcm n2) lcm n3 by A21, A22;
hence x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 by A27, INT_1:15; :: thesis: verum
end;
hence for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 ) by A3, A5; :: thesis: verum