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