List of theorems referencing the symbol DOT_R_LT
(799) Theorem 649: [The reals are a linearly ordered set, 2] ((X in Re) & (Y in Re)) •imp ((X •R_LT Y) or (X = Y) or (Y •R_LT X))
(802) Theorem 652: [The ordering of reals is defined by the sign of their differences] ((((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y))))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X))
(803) Theorem 653: [Various basic properties of real comparison, quantified form] (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GE y) •eq R_is_nonneg(x •R_PLUS R_Rev(y)))) & (FORALL x, y | ((x •R_LE y) •eq (y •R_GE x))) & (FORALL x, y | ((x •R_GT y) •eq ((x •R_GE y) & (x /= y)))) & (FORALL x, y | ((x •R_LT y) •eq (y •R_GT x))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq (R_is_nonneg(y •R_PLUS R_Rev(x))))) & (FORALL x, y | ((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_PLUS R_Rev(y)) & (x /= y)))) & (FORALL x, y | (((x in Re) & (y in Re)) •imp ((x •R_GT y) •eq (R_is_nonneg(x •R_MINUS y) & (x /= y))))) & (FORALL x, y | ((x in Re) & (y in Re) & ((x = y) or (not(x •R_GE y)))) •imp (y •R_GE x))
(804) Theorem 654: [Various basic properties of real comparison] (((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq R_is_nonneg(X •R_PLUS R_Rev(Y)))) & ((X •R_LE Y) •eq (Y •R_GE X)) & ((X •R_GT Y) •eq ((X •R_GE Y) & (X /= Y))) & ((X •R_LT Y) •eq (Y •R_GT X)) & (((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq R_is_nonneg(Y •R_PLUS R_Rev(X)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_PLUS R_Rev(Y)) & (X /= Y)))) & (((X in Re) & (Y in Re)) •imp ((X •R_GT Y) •eq (R_is_nonneg(X •R_MINUS Y) & (X /= Y)))) & (((X in Re) & (Y in Re) & ((X = Y) or (not(X •R_GE Y)))) •imp (Y •R_GE X))
(810) Theorem 660: [Less_than_equal is less-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq ((X •R_LT Y) or (X = Y)))
(811) Theorem 661: [Transitivity of ordering by 'less than'] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LE Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(812) Theorem 662: [Transitivity of ordering by 'less than', 2] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LE Z)) •imp (X •R_LT Z))
(813) Theorem 663: [Transitivity of ordering by 'less than', 3] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(814) Theorem 664: [No real is less than itself] not(X •R_LT X)
(863) Theorem 710: [The embedding of rationals into reals preserves ordering] ((X in Ra) & (Y in Ra)) •imp (((ReRa(X) •R_GE ReRa(Y)) •eq (X •Ra_GE Y)) & ((ReRa(X) •R_GT ReRa(Y)) •eq (X •Ra_GT Y)) & ((ReRa(Y) •R_LE ReRa(X)) •eq (Y •Ra_LE X)) & ((ReRa(Y) •R_LT ReRa(X)) •eq (Y •Ra_LT X)))
(891) Theorem 736: [Every positive real is bounded below by a rational fraction of the form 1/n] ((x in Re) & (x •R_GT R_0)) •imp (EXISTS n in Za | (R_1 •R_OVER ReRa(RaSi(SiZa(n)))) •R_LT x)
(895) Theorem 740: [Any bounded set of reals has a least upper bound] ((S •incin Re) & (S /= 0) & (EXISTS y in Re | (FORALL x in s | y •R_GE x))) •imp (EXISTS u in Re | ((FORALL x in s | u •R_GE x) & (FORALL v in Re | (v •R_LT u •imp (not (FORALL x in s | v •R_GE x))))))