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) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) 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) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) 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) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) gcd (m * n)) ) )
( p = (numerator p) / (denominator p) & q = (numerator q) / (denominator q) ) by RAT_1:15;
hence ( m = denominator p & n = denominator q & i = numerator p & j = numerator q implies ( denominator (p * q) = (m * n) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) gcd (m * n)) ) ) by Th25; :: thesis: verum