let x, y, a, b be Integer; :: thesis: ( x mod a = y mod a & x mod b = y mod b & a,b are_coprime implies x mod (a * b) = y mod (a * b) )
assume A1: ( x mod a = y mod a & x mod b = y mod b & a,b are_coprime ) ; :: thesis: x mod (a * b) = y mod (a * b)
set g1 = x mod a;
set g2 = x mod b;

per cases ( a * b = 0 or a * b <> 0 ) ;

suppose A2: a * b = 0 ; :: thesis: x mod (a * b) = y mod (a * b)

hence x mod (a * b) = 0 by INT_1:def 10
.= y mod (a * b) by A2, INT_1:def 10 ;
:: thesis: verum

end;

suppose a * b <> 0 ; :: thesis: x mod (a * b) = y mod (a * b)

then A3: ( a <> 0 & b <> 0 ) ;
then A4: y = ((y div a) * a) + (y mod a) by INT_1:59;
A5: x = ((x div b) * b) + (x mod b) by A3, INT_1:59;
x - y = (((x div a) * a) + (x mod a)) - (((y div a) * a) + (y mod a)) by A3, A4, INT_1:59
.= ((x div a) - (y div a)) * a by A1 ;
then A6: x,y are_congruent_mod a ;
x - y = (((x div b) * b) + (x mod b)) - (((y div b) * b) + (y mod b)) by A3, A5, INT_1:59
.= ((x div b) - (y div b)) * b by A1 ;
then x,y are_congruent_mod b ;
then x,y are_congruent_mod a * b by A1, A6, INT_6:21;
then consider p being Integer such that
A7: x - y = (a * b) * p ;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
thus x mod (a * b) = (y + ((a * b) * p)) mod (a * b) by A7
.= ((y mod (a * b)) + (((a * b) * p) mod (a * b))) mod (a * b) by NAT_D:66
.= ((y mod (a * b)) + ((((a * b) mod (a * b)) * (p mod (a * b))) mod (a * b))) mod (a * b) by NAT_D:67
.= ((y mod (a * b)) + ((I0 * (p mod (a * b))) mod (a * b))) mod (a * b) by INT_1:50
.= (y + I0) mod (a * b) by NAT_D:66
.= y mod (a * b) ; :: thesis: verum

end;

end;