List of theorems referencing the symbol R_REV

(743) Theorem 592: ({X,Y} •incin Re) •imp (((X •R_PLUS Y) in Re) & (R_Rev(X) in Re))
(752) Theorem 601: [Lemma for law of signs] (X in RaCauchy) •imp (Cauchy_to_Re(Ras_Rev(X)) = R_Rev(Cauchy_to_Re(X)))
(753) Theorem 602: [Law of signs for real multiplication] ({X,Y} •incin Re) •imp (((X •R_TIMES R_Rev(Y)) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES Y) = R_Rev(X •R_TIMES Y)) & ((R_Rev(X) •R_TIMES R_Rev(Y)) = (X •R_TIMES Y)))
(759) Theorem 608: [The zero real is its own negative] R_Rev(R_0) = R_0
(762) Theorem 611: [Basic properties of the signed negative for reals] (X in Re) •imp ((R_Rev(X) in Re) & ((R_Rev(X) •R_PLUS X) = R_0))
(762+) Theorem 612: [Basic properties of the signed negative for reals, 2] (X in Re) •imp (R_Rev(R_Rev(X)) = X)
(764) Theorem 614: [Real subtraction is addition of the negative] ((X in Re) & (Y in Re)) •imp ((X •R_MINUS Y) = (X •R_PLUS R_Rev(Y)))
(765) Theorem 615: [The sum of a real number and its additive inverse is zero] (X in Re) •imp ((R_Rev(X) in Re) & ((X •R_PLUS R_Rev(X)) = R_0))
(766) Theorem 616: [The negative of a real x is zero iff x is zero] (X in Re) •imp ((R_Rev(X) = R_0) •eq (X = R_0))
(767) Theorem 617: [The negative of a real sum is the sum of the negatives] ((X in Re) & (Y in Re)) •imp (R_Rev(X •R_PLUS Y) = R_Rev(X) •R_PLUS R_Rev(Y))
(771) Theorem 621: [Multiplication by R_Rev(R_1)] (X in Re) •imp (R_Rev(X) = R_Rev(R_1) •R_TIMES X)
(773) Theorem 623: [Additive inverse of real difference] ((X in Re) & (Y in Re)) •imp (R_Rev(X •R_MINUS Y) = (Y •R_MINUS X))
(778) Theorem 628: [Reverse of real reciprocal] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Rev(X)) = R_Rev(R_Recip(X)))
(790) Theorem 640: (X in Re) •imp ((R_Rev(X) = Cauchy_to_Re(arb(R_Rev(X)))) & Ra_eqseq(Ras_ABS(arb(X)),arb(Cauchy_to_Re(Ras_ABS(arb(X))))))
(792) Theorem 642: [Any real x or its reverse is non-negative, and if both are non-negative, then x = 0] (X in Re) •imp ((R_is_nonneg(X) or R_is_nonneg(R_Rev(X))) & ((R_is_nonneg(X) & R_is_nonneg(R_Rev(X))) •imp (X = R_0)))
(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))
(815) Theorem 665: [Sign reversal inverts comparisons] ((X in Re) & (Y in Re) & (X •R_GE Y)) •imp (R_Rev(Y) •R_GE R_Rev(X))
(816) Theorem 666: [Sign reversal inverts comparisons,2] ((X in Re) & (Y in Re)) •imp (((X •R_GE Y) •eq (R_Rev(Y) •R_GE R_Rev(X))) & ((X •R_GT Y) •eq (R_Rev(Y) •R_GT R_Rev(X))))
(817) Theorem 667: [Properties of the real zero and unit] (R_Rev(R_0) = R_0) & (R_1 /= R_0) & (R_1 •R_GT R_0) & (R_Recip(R_1) = R_1)
(843) Theorem 690: [Trigger for Otter theory 'orderedGroups'] (R_0 in Re) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) in Re)) & (FORALL x | (x in Re) •imp (R_Rev(x) in Re)) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (((x •R_PLUS y) •R_PLUS z) = (x •R_PLUS (y •R_PLUS z)))) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_0) = x)) & (FORALL x | (x in Re) •imp ((x •R_PLUS R_Rev(x)) = R_0)) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) = (y •R_PLUS x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((R_is_nonneg(x) & R_is_nonneg(y)) •imp R_is_nonneg(x •R_PLUS y))) & (FORALL x | (x in Re) •imp (R_is_nonneg(x) or R_is_nonneg(R_Rev(x)))) & (FORALL x | (x in Re) •imp ((R_is_nonneg(x) & R_is_nonneg(R_Rev(x))) •imp (x = R_0))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_LE y) •eq R_is_nonneg(y •R_PLUS R_Rev(x))))
(844) Theorem 691: [Basic properties of the absolute value function] (FORALL x | abs(x) = if R_is_nonneg(x) then x else R_Rev(x) end if) & (FORALL x | (x in Re) •imp (x •R_LE abs(x))) & (FORALL x | (x in Re) •imp (abs(abs(x)) = abs(x))) & (FORALL x | (x in Re) •imp ((abs(x) = R_0) •eq (x = R_0))) & (FORALL x | (x in Re) •imp (abs(R_Rev(x)) = abs(x))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp ((abs(x •R_PLUS R_Rev(y)) •R_LE z) •imp (y •R_LE (x •R_PLUS z)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x •R_PLUS y) •R_LE (abs(x) •R_PLUS abs(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp ((not(R_is_nonneg(x))) •imp ((x •R_LE abs(y)) & (x /= abs(y))))) & (FORALL x,y,z | ((x in Re) & (y in Re) & (z in Re)) •imp (abs((x •R_PLUS R_Rev(z))) •R_LE (abs(x •R_PLUS R_Rev(y)) •R_PLUS abs(y •R_PLUS R_Rev(z))))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(abs(x) •R_PLUS R_Rev(abs(y))) •R_LE abs(x •R_PLUS R_Rev(y)))) & (FORALL x,y | ((x in Re) & (y in Re)) •imp (abs(x) •R_PLUS R_Rev(abs(abs(y) •R_PLUS R_Rev(abs(x)))) •R_LE abs(y)))
(847) Theorem 694: [The absolute value of x is whichever of x and -x is non-negative, 2] (X in Re) •imp (abs(X) = if R_is_nonneg(R_Rev(X)) then R_Rev(X) else X end if)
(849) Theorem 696: [x and -x have the same absolute value] (X in Re) •imp (abs(X) = abs(R_Rev(X)))
(850) Theorem 697: [Monotonicity of addition, 2] ((X in Re) & (Y in Re) & R_is_nonneg(R_Rev(Y))) •imp ((X •R_GT (X •R_PLUS Y)) or (X = (X •R_PLUS Y)))
(851) Theorem 698: ((X in Re) & (Y in Re) & R_is_nonneg(X) & (not R_is_nonneg(Y))) •imp ((X •R_GE abs(X •R_PLUS Y)) or (R_Rev(Y) •R_GE abs(X •R_PLUS Y)))
(857) Theorem 704: [The embedding of rationals into reals preserves all elementary algebraic operations, 1] (Y in Ra) •imp ((ReRa(Y) in Re) & (ReRa(Ra_Rev(Y)) = R_Rev(ReRa(Y))) & (R_is_nonneg(ReRa(Y)) •eq Ra_is_nonneg(Y)) & (ReRa(Ra_ABS(Y)) = abs(ReRa(Y))))
(874) Theorem 721: [Elementary properties of the real absolute value] ((X in Re) & (Y in Re)) •imp ((abs(X) in Re) & (abs(Y) in Re) & (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y))) & ((abs(X) •R_PLUS abs(Y)) •R_GE abs(X •R_PLUS Y) & (abs(R_Rev(X)) = abs(X))))