let i, j be Integer; :: thesis: ( i,j are_coprime implies i * j divides i lcm j )
assume i,j are_coprime ; :: thesis: i * j divides i lcm j
then |.(i * j).| divides i lcm j by Th15;
then consider z being Integer such that
A1: |.(i * j).| * z = i lcm j by INT_1:def 3;

per cases ( 0 <= i * j or 0 > i * j ) ;

suppose 0 <= i * j ; :: thesis: i * j divides i lcm j

then z * (i * j) = i lcm j by A1, ABSVALUE:def 1;
hence i * j divides i lcm j by INT_1:def 3; :: thesis: verum

end;

suppose A2: 0 > i * j ; :: thesis: i * j divides i lcm j

(- z) * (i * j) = z * (- (i * j))
.= i lcm j by A1, A2, ABSVALUE:def 1 ;
hence i * j divides i lcm j by INT_1:def 3; :: thesis: verum

end;

end;