theorem Th31: :: RING_3:31

for p being Rational
for m being Nat
for i being Integer st m = denominator p & i = numerator p holds
( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) )