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

( 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