let a, b be Integer; :: thesis: |.(a * b).| = (a gcd b) * (a lcm b)
|.(a * b).| = |.a.| * |.b.| by COMPLEX1:65
.= (|.a.| gcd |.b.|) * (|.a.| lcm |.b.|) by NAT_D:29
.= (a gcd b) * (|.a.| lcm |.b.|) by INT_2:34
.= (a gcd b) * (a lcm b) by INT_2:33 ;
hence |.(a * b).| = (a gcd b) * (a lcm b) ; :: thesis: verum