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).|
per cases ( i = 0 or j = 0 or ( i <> 0 & j <> 0 ) ) ;
suppose A2: ( i = 0 or j = 0 ) ; :: thesis: i lcm j = |.(i * j).|
hence i lcm j = 0 by INT_2:4
.= |.(i * j).| by A2, ABSVALUE:2 ;
:: thesis: verum
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
proof
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;
per cases ( kij = 1 or kij = - 1 ) by A10, INT_2:13;
suppose A14: kij = - 1 ; :: thesis: |.(i * j).| divides m
- (i * j) <> 0 by A3, XCMPLX_1:6;
then - (- (i * j)) < 0 by A8, A14;
hence |.(i * j).| divides m by A8, A13, A14, ABSVALUE:def 1; :: thesis: verum
end;
end;
end;
j divides |.j.| by Th13;
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;
end;