let p, q be Rational; :: thesis: for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds
( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )
let m1, m2, n1, n2 be Nat; :: thesis: ( m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 implies ( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) ) )
assume A1: ( m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 ) ; :: thesis: ( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )
hence denominator (p / q) = (m1 * n2) div ((n1 * m2) gcd (m1 * n2)) by Th41
.= (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) by Th8 ;
:: thesis: numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2))
thus numerator (p / q) = (n1 * m2) div ((n1 * m2) gcd (m1 * n2)) by A1, Th41
.= (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) by Th7 ; :: thesis: verum