let x, y, i, j be Integer; :: thesis: ( i,j are_relative_prime & x,y are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i * j )
assume i,j are_relative_prime ; :: 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:19;
i divides x - y by A2, INT_2:19;
then i lcm j divides x - y by A4, INT_2:27;
then i * j divides x - y by A1, INT_2:13;
hence x,y are_congruent_mod i * j by INT_2:19; :: thesis: verum