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 * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )
let i, j be Integer; :: thesis: ( m <> 0 & n <> 0 implies ( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) ) )
assume that
A1: m <> 0 and
A2: n <> 0 ; :: thesis: ( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )
(i / m) + (j / n) = ((i * n) / (m * n)) + (j / n) by A2, XCMPLX_1:91
.= ((i * n) / (m * n)) + ((j * m) / (m * n)) by A1, XCMPLX_1:91
.= ((i * n) + (j * m)) / (m * n) ;
hence ( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) ) by A1, A2, Th15; :: thesis: verum