let m, n be Nat; :: thesis: for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) + (j / n)) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((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) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) ) )
assume A1: ( m <> 0 & n <> 0 ) ; :: thesis: ( denominator ((i / m) + (j / n)) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
hence denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) by Th21
.= (m * n) / (((i * n) + (j * m)) gcd (m * n)) by Th8 ;
:: thesis: numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n))
thus numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) by A1, Th21
.= ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) by Th7 ; :: thesis: verum