List of theorems referencing the symbol DOT_RA_LT

(598) Theorem 450: [?] (FORALL x,y | ((x •Ra_GE y) •eq Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x •Ra_LE y) •eq (y •Ra_GE x))) & (FORALL x,y | ((x •Ra_GT y) •eq ((x •Ra_GE y) & (x /= y)))) & (FORALL x,y | ((x •Ra_LT y) •eq (y •Ra_GT x))) & (FORALL x,y | ((x •Ra_LE y) •eq Ra_is_nonneg(y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | (((x in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_PLUS Ra_Rev(y)) & (x /= y))))) & (FORALL x,y | (((y in Ra) & (y in Ra)) •imp ((x •Ra_GT y) •eq (Ra_is_nonneg(x •Ra_MINUS y) & (x /= y))))) & (FORALL x,y | (((x in Ra) & (y in Ra) & ((x = y) or (not(x •Ra_GE y)))) •imp (y •Ra_GE x)))
(599) Theorem 451: [Various basic properties of rational comparison] ((X •Ra_GE Y) •eq Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y))) & ((X •Ra_LE Y) •eq (Y •Ra_GE X)) & ((X •Ra_GT Y) •eq ((X •Ra_GE Y) & (X /= Y))) & ((X •Ra_LT Y) •eq (Y •Ra_GT X)) & ((X •Ra_LE Y) •eq Ra_is_nonneg(Y •Ra_PLUS Ra_Rev(X))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_PLUS Ra_Rev(Y)) & (X /= Y)))) & (((X in Ra) & (Y in Ra)) •imp ((X •Ra_GT Y) •eq (Ra_is_nonneg(X •Ra_MINUS Y) & (X /= Y)))) & (((X in Ra) & (Y in Ra) & ((X = Y) or (not(X •Ra_GE Y)))) •imp (Y •Ra_GE X))
(601) Theorem 453: [Less_than_equal is less-than and equal] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LE Y) •eq ((X •Ra_LT Y) or (X = Y)))
(603) Theorem 455: [The rationals are a linearly ordered set, 2] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (X = Y) or (Y •Ra_LT X))
(605) Theorem 457: [The rationals are a linearly ordered set,4] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_LT Y) or (Y •Ra_LE X))
(627) Theorem 480: [Transitivity of ordering by 'less than'] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LE Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(628) Theorem 481: [Transitivity of ordering by 'less than', 2] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LE Z)) •imp (X •Ra_LT Z))
(629) Theorem 482: [Transitivity of ordering by 'less than', 3] ((X in Ra) & (Y in Ra) & (Z in Ra)) •imp (((X •Ra_LT Y) & (Y •Ra_LT Z)) •imp (X •Ra_LT Z))
(640) Theorem 493: (FORALL x in Ra, y in Ra, z in Ra | ((x •Ra_LT y) & (y •Ra_LT z)) •imp (x •Ra_LT z))
(641) Theorem 494: (FORALL x in Ra | not(x •Ra_LT x))
(642) Theorem 495: (FORALL x in Ra, y in Ra | (x •Ra_LT y) or (x = y) or (y •Ra_LT x))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_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)))
(869) Theorem 716: [The embedding of signed integers into rationals preserves ordering] ((X in Si) & (Y in Si)) •imp (((RaSi(X) •Ra_GE RaSi(Y)) •eq (X •S_GE Y)) & ((RaSi(X) •Ra_GT RaSi(Y)) •eq (X •S_GT Y)) & ((RaSi(Y) •Ra_LE RaSi(X)) •eq (Y •S_LE X)) & ((RaSi(Y) •Ra_LT RaSi(X)) •eq (Y •S_LT X)))