let x, y, i, j be Integer; :: thesis: ( i,j are_coprime & x,y are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i * j )
assume i,j are_coprime ; :: thesis: ( not x,y are_congruent_mod i or not x,y are_congruent_mod j or x,y are_congruent_mod i * j )
then A1: i * j divides i lcm j by Th20;
assume that
A2: x,y are_congruent_mod i and
A3: x,y are_congruent_mod j ; :: thesis: x,y are_congruent_mod i * j
A4: j divides x - y by A3, INT_2:15;
i divides x - y by A2, INT_2:15;
then i lcm j divides x - y by A4, INT_2:19;
then i * j divides x - y by A1, INT_2:9;
hence x,y are_congruent_mod i * j by INT_2:15; :: thesis: verum