let p be Rational; :: thesis: ( p < - 1 iff numerator p < - (denominator p) )

hereby :: thesis: ( numerator p < - (denominator p) implies p < - 1 )

assume p < - 1 ; :: thesis: numerator p < - (denominator p)
then (numerator p) / (denominator p) < - 1 by Th12;
then ((numerator p) / (denominator p)) * (denominator p) < (- 1) * (denominator p) by XREAL_1:68;
hence numerator p < - (denominator p) by XCMPLX_1:87; :: thesis: verum

end;

assume numerator p < - (denominator p) ; :: thesis: p < - 1
then (numerator p) * ((denominator p) ") < ((- 1) * (denominator p)) * ((denominator p) ") by XREAL_1:68;
then (numerator p) * ((denominator p) ") < (- 1) * ((denominator p) * ((denominator p) ")) ;
then (numerator p) * ((denominator p) ") < (- 1) * 1 by XCMPLX_0:def 7;
hence p < - 1 by Th12; :: thesis: verum