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