let i, j be Integer; :: thesis: ( i,j are_coprime implies i lcm j = |.(i * j).| )

assume A1: i gcd j = 1 ; :: according to INT_2:def 3 :: thesis: i lcm j = |.(i * j).|

assume A1: i gcd j = 1 ; :: according to INT_2:def 3 :: thesis: i lcm j = |.(i * j).|

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

end;

suppose A3:
( i <> 0 & j <> 0 )
; :: thesis: i lcm j = |.(i * j).|

A4:
for m being Integer st i divides m & j divides m holds

|.(i * j).| divides m

then j divides |.i.| * |.j.| by INT_2:2;

then A15: j divides |.(i * j).| by COMPLEX1:65;

i divides |.i.| by Th13;

then i divides |.i.| * |.j.| by INT_2:2;

then i divides |.(i * j).| by COMPLEX1:65;

hence i lcm j = |.(i * j).| by A15, A4, INT_2:def 1; :: thesis: verum

end;|.(i * j).| divides m

proof

j divides |.j.|
by Th13;
j divides i lcm j
by INT_2:def 1;

then consider kj being Integer such that

A5: j * kj = i lcm j by INT_1:def 3;

i divides i lcm j by INT_2:def 1;

then consider ki being Integer such that

A6: i * ki = i lcm j by INT_1:def 3;

A7: j divides i * j by INT_2:2;

i divides i * j by INT_2:2;

then i lcm j divides i * j by A7, INT_2:def 1;

then consider kij being Integer such that

A8: (i lcm j) * kij = i * j by INT_1:def 3;

i * j = j * (kj * kij) by A5, A8;

then i = kj * kij by A3, XCMPLX_1:5;

then A9: kij divides i by INT_1:def 3;

i * j = i * (ki * kij) by A6, A8;

then j = ki * kij by A3, XCMPLX_1:5;

then kij divides j by INT_1:def 3;

then A10: kij divides 1 by A1, A9, INT_2:def 2;

let m be Integer; :: thesis: ( i divides m & j divides m implies |.(i * j).| divides m )

assume that

A11: i divides m and

A12: j divides m ; :: thesis: |.(i * j).| divides m

A13: i lcm j divides m by A11, A12, INT_2:def 1;

end;then consider kj being Integer such that

A5: j * kj = i lcm j by INT_1:def 3;

i divides i lcm j by INT_2:def 1;

then consider ki being Integer such that

A6: i * ki = i lcm j by INT_1:def 3;

A7: j divides i * j by INT_2:2;

i divides i * j by INT_2:2;

then i lcm j divides i * j by A7, INT_2:def 1;

then consider kij being Integer such that

A8: (i lcm j) * kij = i * j by INT_1:def 3;

i * j = j * (kj * kij) by A5, A8;

then i = kj * kij by A3, XCMPLX_1:5;

then A9: kij divides i by INT_1:def 3;

i * j = i * (ki * kij) by A6, A8;

then j = ki * kij by A3, XCMPLX_1:5;

then kij divides j by INT_1:def 3;

then A10: kij divides 1 by A1, A9, INT_2:def 2;

let m be Integer; :: thesis: ( i divides m & j divides m implies |.(i * j).| divides m )

assume that

A11: i divides m and

A12: j divides m ; :: thesis: |.(i * j).| divides m

A13: i lcm j divides m by A11, A12, INT_2:def 1;

then j divides |.i.| * |.j.| by INT_2:2;

then A15: j divides |.(i * j).| by COMPLEX1:65;

i divides |.i.| by Th13;

then i divides |.i.| * |.j.| by INT_2:2;

then i divides |.(i * j).| by COMPLEX1:65;

hence i lcm j = |.(i * j).| by A15, A4, INT_2:def 1; :: thesis: verum