let p be Rational; :: thesis: ( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )
A2: p = - (- p)
.= - ((numerator (- p)) / (denominator (- p))) by Th12
.= (- (numerator (- p))) / (denominator (- p)) ;
consider w being Nat such that
- (numerator (- p)) = (numerator p) * w and
A3: denominator (- p) = (denominator p) * w by A2, Th24;
- p = - ((numerator p) / (denominator p)) by Th12
.= (- (numerator p)) / (denominator p) ;
then consider k being Nat such that
A4: - (numerator p) = (numerator (- p)) * k and
A5: denominator p = (denominator (- p)) * k by Th24;
denominator p = ((denominator p) * w) * k by A5, A3
.= (denominator p) * (w * k) ;
then A6: k = 1 by NAT_1:15, XCMPLX_1:7;
hence denominator p = denominator (- p) by A5; :: thesis: numerator (- p) = - (numerator p)
thus numerator (- p) = - (numerator p) by A4, A6; :: thesis: verum