let p be Rational; :: thesis: ( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )
A1: denominator p <> 0 by Def3;
A2: p = - (- p)
.= - ((numerator (- p)) / (denominator (- p))) by Th37
.= (- (numerator (- p))) / (denominator (- p)) ;
denominator (- p) <> 0 by Def3;
then consider l being Element of NAT such that
- (numerator (- p)) = (numerator p) * l and
A3: denominator (- p) = (denominator p) * l by A2, Th60;
- p = - ((numerator p) / (denominator p)) by Th37
.= (- (numerator p)) / (denominator p) ;
then consider k being Element of NAT such that
A4: - (numerator p) = (numerator (- p)) * k and
A5: denominator p = (denominator (- p)) * k by A1, Th60;
denominator p = ((denominator p) * l) * k by A5, A3
.= (denominator p) * (l * k) ;
then A6: k = 1 by A1, 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