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 A1: ( m1 <> 0 & m2 <> 0 & 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 )
given x being Integer such that A2: ( (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 ) ; :: thesis: contradiction
A3: ( m1 divides x - c1 & m2 divides x - c2 ) by A1, A2, Lm10;
( m1 gcd m2 divides m1 & m1 gcd m2 divides m2 ) by INT_2:31;
then ( m1 gcd m2 divides x - c1 & m1 gcd m2 divides x - c2 ) by A3, INT_2:13;
then m1 gcd m2 divides (x - c2) - (x - c1) by Lm4;
hence contradiction by A1; :: thesis: verum