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;
A3: now :: thesis: for m being Integer st |.a.| divides m & |.b.| divides m holds
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;
b divides a lcm b by Def1;
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