let m be Nat; :: thesis: for i being Integer st m <> 0 holds
( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )
let i be Integer; :: thesis: ( m <> 0 implies ( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) ) )
assume A1: m <> 0 ; :: thesis: ( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )
hence denominator ((m / i) ") = m div (m gcd i) by Th19
.= m / (m gcd i) by Th8 ;
:: thesis: numerator ((m / i) ") = i / (m gcd i)
thus numerator ((m / i) ") = i div (m gcd i) by A1, Th19
.= i / (m gcd i) by Th7 ; :: thesis: verum