theorem NATD29: :: NEWTON03:7
for a, b being Integer holds |.(a * b).| = (a gcd b) * (a lcm b)