let m be Nat; :: thesis: for i being Integer st m <> 0 holds
( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) )
let i be Integer; :: thesis: ( m <> 0 implies ( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) ) )
(m / i) " = i / m by XCMPLX_1:213;
hence ( m <> 0 implies ( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) ) ) by Th15; :: thesis: verum