let p be Rational; :: thesis: 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) )
let m be Nat; :: thesis: 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) )
let i be Integer; :: thesis: ( m = denominator p & i = numerator p implies ( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) ) )
p = (numerator p) / (denominator p) by RAT_1:15;
hence ( m = denominator p & i = numerator p implies ( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) ) ) by Th17; :: thesis: verum