let a, b be Integer; :: thesis: a lcm b = |.a.| lcm |.b.|

A1: ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

A2: ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

then A4: |.b.| divides a lcm b by A1, Th10;

a divides a lcm b by Def1;

then |.a.| divides a lcm b by A2, Th10;

hence a lcm b = |.a.| lcm |.b.| by A4, A3, Def1; :: thesis: verum

A1: ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

A2: ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

A3: now :: thesis: for m being Integer st |.a.| divides m & |.b.| divides m holds

a lcm b divides m

b divides a lcm b
by Def1;a lcm b divides m

let m be Integer; :: thesis: ( |.a.| divides m & |.b.| divides m implies a lcm b divides m )

assume ( |.a.| divides m & |.b.| divides m ) ; :: thesis: a lcm b divides m

then ( a divides m & b divides m ) by A2, A1, Th10;

hence a lcm b divides m by Def1; :: thesis: verum

end;assume ( |.a.| divides m & |.b.| divides m ) ; :: thesis: a lcm b divides m

then ( a divides m & b divides m ) by A2, A1, Th10;

hence a lcm b divides m by Def1; :: thesis: verum

then A4: |.b.| divides a lcm b by A1, Th10;

a divides a lcm b by Def1;

then |.a.| divides a lcm b by A2, Th10;

hence a lcm b = |.a.| lcm |.b.| by A4, A3, Def1; :: thesis: verum