let p, q be Rational; :: thesis: for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
let m, n be Nat; :: thesis: for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
let i, j be Integer; :: thesis: ( m = denominator p & n = denominator q & i = numerator p & j = numerator q implies ( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) ) )
assume A1: ( m = denominator p & n = denominator q & i = numerator p & j = numerator q ) ; :: thesis: ( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
hence denominator (p + q) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) by Th35
.= (m * n) / (((i * n) + (j * m)) gcd (m * n)) by Th8 ;
:: thesis: numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n))
thus numerator (p + q) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) by A1, Th35
.= ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) by Th7 ; :: thesis: verum