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