let m1, m2, c1, c2 be Integer; :: thesis: ( m1 <> 0 & m2 <> 0 & not m1 gcd m2 divides c1 - c2 implies for x being Integer holds
( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 ) )
assume that
A1: m1 <> 0 and
A2: m2 <> 0 and
A3: not m1 gcd m2 divides c1 - c2 ; :: thesis: for x being Integer holds
( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 )
A4: m1 gcd m2 divides m2 by INT_2:21;
given x being Integer such that A5: (x - c1) mod m1 = 0 and
A6: (x - c2) mod m2 = 0 ; :: thesis: contradiction
m2 divides x - c2 by A2, A6, Lm10;
then A7: m1 gcd m2 divides x - c2 by A4, INT_2:9;
A8: m1 gcd m2 divides m1 by INT_2:21;
m1 divides x - c1 by A1, A5, Lm10;
then m1 gcd m2 divides x - c1 by A8, INT_2:9;
then m1 gcd m2 divides (x - c2) - (x - c1) by A7, Lm4;
hence contradiction by A3; :: thesis: verum