let i, j be Integer; :: thesis: ( i,j are_relative_prime implies i lcm j = abs (i * j) )
assume AS: i gcd j = 1 ; :: according to INT_2:def 4 :: thesis: i lcm j = abs (i * j)

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

suppose A: ( i = 0 or j = 0 ) ; :: thesis: i lcm j = abs (i * j)

hence i lcm j = 0 by INT_2:4
.= abs (i * j) by A, ABSVALUE:7 ;
:: thesis: verum

end;

suppose A: ( i <> 0 & j <> 0 ) ; :: thesis: i lcm j = abs (i * j)

i divides abs i by thabs0;
then i divides (abs i) * (abs j) by INT_2:2;
then X: i divides abs (i * j) by COMPLEX1:151;
j divides abs j by thabs0;
then j divides (abs i) * (abs j) by INT_2:2;
then Y: j divides abs (i * j) by COMPLEX1:151;
for m being Integer st i divides m & j divides m holds
abs (i * j) divides m

proof

let m be Integer; :: thesis: ( i divides m & j divides m implies abs (i * j) divides m )
assume B: ( i divides m & j divides m ) ; :: thesis: abs (i * j) divides m
i divides i lcm j by INT_2:def 2;
then consider ki being Integer such that
C: i * ki = i lcm j by INT_1:def 9;
j divides i lcm j by INT_2:def 2;
then consider kj being Integer such that
D: j * kj = i lcm j by INT_1:def 9;
( i divides i * j & j divides i * j ) by INT_2:2;
then i lcm j divides i * j by INT_2:def 2;
then consider kij being Integer such that
E: (i lcm j) * kij = i * j by INT_1:def 9;
i * j = i * (ki * kij) by C, E;
then F: j = ki * kij by A, XCMPLX_1:5;
i * j = j * (kj * kij) by D, E;
then G: i = kj * kij by A, XCMPLX_1:5;
( kij divides i & kij divides j ) by F, G, INT_1:def 9;
then I: kij divides 1 by AS, INT_2:def 3;
K: i lcm j divides m by B, INT_2:def 2;

per cases ( kij = 1 or kij = - 1 ) by I, INT_2:17;

suppose kij = 1 ; :: thesis: abs (i * j) divides m

hence abs (i * j) divides m by E, K, ABSVALUE:def 1; :: thesis: verum

end;

suppose J: kij = - 1 ; :: thesis: abs (i * j) divides m

- (i * j) <> 0 by A, XCMPLX_1:6;
then - (i * j) > 0 by J, E;
then - (- (i * j)) < 0 ;
hence abs (i * j) divides m by J, E, K, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

hence i lcm j = abs (i * j) by X, Y, INT_2:def 2; :: thesis: verum

end;

end;