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 Th17
.= 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, Th17
.= (- i) / ((- i) gcd m) by Th7 ; :: thesis: verum