let x, y, i, j be Integer; ( 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
; ( 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
; 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; verum