List of theorems referencing the symbol RA_REV

(583) Theorem 435: [The sum of a rational number and its additive inverse is zero] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((M •Ra_PLUS Ra_Rev(M)) = Ra_0))
(584) Theorem 436: [The sum of a rational number and its additive inverse is zero, 2] (M in Ra) •imp ((Ra_Rev(M) in Ra) & ((Ra_Rev(M) •Ra_PLUS M) = Ra_0))
(597) Theorem 449: [One of a rational and its additive inverse is always non-negative, and both are non-negative only if the rational is zero] (X in Ra) •imp ((Ra_is_nonneg(X) or Ra_is_nonneg(Ra_Rev(X))) & ((Ra_is_nonneg(X) & Ra_is_nonneg(Ra_Rev(X))) •imp (X = Ra_0)))
(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))
(610) Theorem 462: [Properties of the rational zero and unit] (Ra_Rev(Ra_0) = Ra_0) & (Ra_1 /= Ra_0) & (Ra_1 •Ra_GT Ra_0)
(613) Theorem 465: [Alternate form of Theorem 464] ((X in Si) & (Y in Si) & (Y /= [0,0])) •imp (Ra_Rev(Fr_to_Ra([X,Y])) = Fr_to_Ra([S_Rev(X),Y]))
(614) Theorem 466: [First law of signs for rational multiplication] ((X in Ra) & (Y in Ra)) •imp ((X •Ra_TIMES Ra_Rev(Y)) = Ra_Rev(X •Ra_TIMES Y))
(615) Theorem 467: [The reverse of a rational X is the reverse of 1, times X] (X in Ra) •imp (Ra_Rev(X) = (Ra_Rev(Ra_1) •Ra_TIMES X))
(620) Theorem 473: ((X in Ra) & (Y in Ra)) •imp (Ra_Rev(X •Ra_PLUS Y) = (Ra_Rev(X) •Ra_PLUS Ra_Rev(Y)))
(622) Theorem 475: (X in Ra) •imp (Ra_Rev(Ra_Rev(X)) = X)
(630) Theorem 483: ((X in Ra) & (Y in Ra) & (X •Ra_GE Y)) •imp (Ra_Rev(Y) •Ra_GE Ra_Rev(X))
(631) Theorem 484: ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp (Ra_Rev(Y) •Ra_GT Ra_Rev(X))
(653) Theorem 506: [?] (FORALL x | Ra_ABS(x) = if Ra_is_nonneg(x) then x else Ra_Rev(x) end if) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS y) = (x •Ra_PLUS z)) •imp (y = z))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_Rev(x •Ra_PLUS Ra_Rev(y)) = (y •Ra_PLUS Ra_Rev(x)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_LE y) or (y •Ra_LE x))) & (FORALL x | (x in Ra) •imp (x •Ra_LE x)) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z)) •imp (x •Ra_LE z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y) & (y •Ra_LE z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (y •Ra_LE z) & (y /= z)) •imp (x /= z))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((x •Ra_LE y) •imp ((x •Ra_PLUS z) •Ra_LE (y •Ra_PLUS z)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_PLUS z) = (y •Ra_PLUS z)) •imp (x = y))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (((x •Ra_LE y) & (x /= y)) •imp ((x •Ra_PLUS z) /= (y •Ra_PLUS z)))) & (FORALL x | (x in Ra) •imp (Ra_ABS(x •Ra_PLUS Ra_Rev(x)) = Ra_0)) & (FORALL x | (x in Ra) •imp (x •Ra_LE Ra_ABS(x))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_ABS(x)) = Ra_ABS(x))) & (FORALL x | (x in Ra) •imp ((Ra_ABS(x) = Ra_0) •eq (x = Ra_0))) & (FORALL x | (x in Ra) •imp (Ra_ABS(Ra_Rev(x)) = Ra_ABS(x))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp ((Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_LE z) •imp (y •Ra_LE (x •Ra_PLUS z)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x •Ra_PLUS y) •Ra_LE (Ra_ABS(x) •Ra_PLUS Ra_ABS(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp ((not(Ra_is_nonneg(x))) •imp ((x •Ra_LE Ra_ABS(y)) & (x /= Ra_ABS(y))))) & (FORALL x,y,z | ((x in Ra) & (y in Ra) & (z in Ra)) •imp (Ra_ABS((x •Ra_PLUS Ra_Rev(z))) •Ra_LE (Ra_ABS(x •Ra_PLUS Ra_Rev(y)) •Ra_PLUS Ra_ABS(y •Ra_PLUS Ra_Rev(z))))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_is_nonneg(y) •imp ((x •Ra_PLUS Ra_Rev(y)) •Ra_LE (x •Ra_PLUS y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(y))) •Ra_LE Ra_ABS(x •Ra_PLUS Ra_Rev(y)))) & (FORALL x,y | ((x in Ra) & (y in Ra)) •imp (Ra_ABS(x) •Ra_PLUS Ra_Rev(Ra_ABS(Ra_ABS(y) •Ra_PLUS Ra_Rev(Ra_ABS(x)))) •Ra_LE Ra_ABS(y)))
(686) Theorem 535: ({F,G} •incin RaSeq) •imp (((F •Ras_PLUS G) in RaSeq) & (Ras_ABS(G) in RaSeq) & (Ras_Rev(G) in RaSeq) & ((F •Ras_TIMES G) in RaSeq) & ((F •Ras_PLUS G) = {[u,((F~[u]) •Ra_PLUS (G~[u]))]: u in Za}) & (Ras_ABS(G) = {[u,Ra_ABS(G~[u])]: u in Za}) & (Ras_Rev(G) = {[u,Ra_Rev(G~[u])]: u in Za}) & ((F •Ras_TIMES G) = {[u,((F~[u]) •Ra_TIMES (G~[u]))]: u in Za}))
(687) Theorem 536: (({F1,G1} •incin RaSeq) & (N in Za)) •imp ((F1~[N] in Ra) & (G1~[N] in Ra) & ((F1 •Ras_PLUS G1 in RaSeq) & ((F1 •Ras_PLUS G1)~[N] = (F1~[N]) •Ra_PLUS (G1~[N]))) & (((Ras_ABS(G1) in RaSeq) & (Ras_ABS(G1)~[N] = Ra_ABS(G1~[N])))) & (((Ras_Rev(G1) in RaSeq) & (Ras_Rev(G1)~[N] = Ra_Rev(G1~[N])))) & (((F1 •Ras_TIMES G1 in RaSeq) & (F1 •Ras_TIMES G1)~[N] = ((F1~[N]) •Ra_TIMES (G1~[N])))))
(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))))
(865) Theorem 711: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 1] (X in Si) •imp ((RaSi(X) in Ra) & (Ra_is_nonneg(RaSi(X)) •eq is_nonneg(X)) & (RaSi(S_Rev(X)) = Ra_Rev(RaSi(X))) & (RaSi(S_ABS(X)) = Ra_ABS(RaSi(X))))