let m, n be Nat; :: thesis: for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) )
let i, j be Integer; :: thesis: ( m <> 0 & n <> 0 implies ( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) ) )
(i / m) * (j / n) = (i * j) / (m * n) by XCMPLX_1:76;
hence ( m <> 0 & n <> 0 implies ( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) ) ) by Th15; :: thesis: verum