let a, b be real number ; :: thesis: ( a > 1 & b < 0 implies a #R b < 1 )
assume that
A1: a > 1 and
A2: b < 0 ; :: thesis: a #R b < 1
- b > 0 by A2, XREAL_1:58;
then a #R (- b) > 1 by A1, Th100;
then 1 / (a #R b) > 1 by A1, Th90;
then 1 / (1 / (a #R b)) < 1 by XREAL_1:212;
hence a #R b < 1 ; :: thesis: verum