List of theorems referencing the symbol DOT_RA_PLUS

(570) Theorem 421: [The sum of a rational number and a formal fraction can be expressed as a sum of formal fractions] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (X •Ra_PLUS Fr_to_Ra([Y,Z]) = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(577) Theorem 428: [Commutativity of rational addition] ((N in Ra) & (M in Ra)) •imp ((N •Ra_PLUS M in Ra) & (N •Ra_PLUS M = M •Ra_PLUS N))
(578) Theorem 429: [?] ((X in Ra) & (Y in Si) & (Z in Si) & (Z /= [0,0])) •imp (Fr_to_Ra([Y,Z]) •Ra_PLUS X = Fr_to_Ra([(car(arb(X)) •S_TIMES Z) •S_PLUS (cdr(arb(X)) •S_TIMES Y),(cdr(arb(X)) •S_TIMES Z)]))
(578+) Theorem 430: [?] ((X in Si) & (Y in Si) & (Z in Si) & (W in Si) & (Y /= [0,0]) & (W /= [0,0])) •imp (Fr_to_Ra([X,Y]) •Ra_PLUS Fr_to_Ra([Z,W]) = Fr_to_Ra([(X •S_TIMES W) •S_PLUS (Z •S_TIMES Y),Y •S_TIMES W]))
(581) Theorem 433: [Associative law for rational addition] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_PLUS (M •Ra_PLUS K) = (N •Ra_PLUS M) •Ra_PLUS K)
(582) Theorem 434: [The zero rational is the identity for rational addition] (Ra_0 in Ra) & (Ra_1 in Ra) & ((M in Ra) •imp (M = M •Ra_PLUS Ra_0))
(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))
(586) Theorem 438: [Rational subtraction is equivalent to addition of the rational negative] ((N in Ra) & (M in Ra)) •imp (N = M •Ra_PLUS (N •Ra_MINUS M))
(589) Theorem 441: [Distributive law for rationals] ((K in Ra) & (N in Ra) & (M in Ra)) •imp (N •Ra_TIMES (M •Ra_PLUS K) = (N •Ra_TIMES M) •Ra_PLUS (N •Ra_TIMES K))
(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))
(608) Theorem 460: [The sum and product of two non-negative rationals is non-negative] ((X in Ra) & (Y in Ra) & Ra_is_nonneg(X) & Ra_is_nonneg(Y)) •imp (Ra_is_nonneg(X •Ra_PLUS Y) & Ra_is_nonneg(X •Ra_TIMES Y))
(620) Theorem 473: ((X in Ra) & (Y in Ra)) •imp (Ra_Rev(X •Ra_PLUS Y) = (Ra_Rev(X) •Ra_PLUS Ra_Rev(Y)))
(621) Theorem 474: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GE (Y •Ra_PLUS YP))
(632) Theorem 485: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GE Y) & (XP •Ra_GT YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(633) Theorem 486: ((X in Ra) & (Y in Ra) & (XP in Ra) & (YP in Ra) & (X •Ra_GT Y) & (XP •Ra_GE YP)) •imp ((X •Ra_PLUS XP) •Ra_GT (Y •Ra_PLUS YP))
(647) Theorem 500: [The average of two rational numbers lies between them] ((X in Ra) & (Y in Ra) & (X •Ra_GT Y)) •imp ((X •Ra_GT ((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))) & (((X •Ra_PLUS Y) •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_GT Y))
(648) Theorem 501: [Properties of the rational number 2] ((Ra_1 •Ra_PLUS Ra_1) in Ra) & ((Ra_1 •Ra_PLUS Ra_1) •Ra_GT Ra_0) & (Recip(Ra_1 •Ra_PLUS Ra_1) in Ra) & ((X in Ra) •imp ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) in Ra))
(649) Theorem 502: [Any rational number can be divided into two equal halves] (X in Ra) •imp (X = ((X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1)) •Ra_PLUS (X •Ra_OVER (Ra_1 •Ra_PLUS Ra_1))))
(650) Theorem 503: [Every positive rational exceeds the sum of two smaller positive rationals] ((X in Ra) & (X •Ra_GT Ra_0)) •imp (EXISTS e in Ra, e0 in Ra | (X •Ra_GT e) & (e •Ra_GT e0) & (e0 •Ra_GT Ra_0) & (e •Ra_GT Ra_0) & (X •Ra_GT (e •Ra_PLUS e0)))
(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)))
(662) Theorem 515: [Formula for the sum of two rational quotients] ((X in Ra) & (Y in Ra) & (U in Ra) & (V in Ra) & (X /= Ra_0) & (Y /= Ra_0)) •imp (((U •Ra_OVER X) •Ra_PLUS (V •Ra_OVER Y)) = (((Y •Ra_TIMES U) •Ra_PLUS (X •Ra_TIMES V)) •Ra_OVER (X •Ra_TIMES 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])))))
(858) Theorem 705: [The embedding of rationals into reals preserves all elementary algebraic operations, 2] ((X in Ra) & (Y in Ra)) •imp ((ReRa(X) in Re) & (ReRa(Y) in Re) & (ReRa(X •Ra_PLUS Y) = ReRa(X) •R_PLUS ReRa(Y)) & (ReRa(X •Ra_TIMES Y) = ReRa(X) •R_TIMES ReRa(Y)))
(866) Theorem 712: [The embedding of signed integers into rationals preserves all elementary algebraic operations, 2] ((X in Si) & (Y in Si)) •imp ((RaSi(X) in Ra) & (RaSi(Y) in Ra) & (RaSi(X •S_PLUS Y) = RaSi(X) •Ra_PLUS RaSi(Y)) & (RaSi(X •S_TIMES Y) = RaSi(X) •Ra_TIMES RaSi(Y)))