List of theorems referencing the symbol DOT_R_PLUS
(743) Theorem 592: ({X,Y} •incin Re) •imp (((X •R_PLUS Y) in Re) & (R_Rev(X) in Re))
(745) Theorem 594: [Commutative law for real addition] ({X,Y} •incin Re) •imp ((X •R_PLUS Y) = (Y •R_PLUS X))
(746) Theorem 595: [Elementary algebraic lemma for real addition] ((X in RaCauchy) & (Y in RaCauchy)) •imp (Cauchy_to_Re(X •Ras_PLUS Y) = (Cauchy_to_Re(X) •R_PLUS Cauchy_to_Re(Y)))
(747) Theorem 596: [Associative law for real addition] ({X,Y,V} •incin Re) •imp ((X •R_PLUS (Y •R_PLUS V)) = ((X •R_PLUS Y) •R_PLUS V))
(751) Theorem 600: [Distributive law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_PLUS V)) = ((X •R_TIMES Y) •R_PLUS (X •R_TIMES V)))
(756) Theorem 605: [0 is a right and left additive identity for reals] (X in Re) •imp ((X •R_PLUS R_0 = X) & (R_0 •R_PLUS X = X))
(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))
(763) Theorem 613: [Real additive Cancellation] ((X in Re) & (Y in Re) & (V in Re) & (X •R_PLUS V = Y •R_PLUS V)) •imp (X = Y)
(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))
(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))
(768) Theorem 618: [Real addition-subtraction commutativity] ((X in Re) & (Y in Re) & (V in Re)) •imp (X •R_MINUS (Y •R_PLUS V) = (X •R_MINUS Y) •R_MINUS V)
(769) Theorem 619: [Real subtraction reverses addition] ((X in Re) & (Y in Re)) •imp ((X •R_PLUS Y) •R_MINUS Y = X)
(770) Theorem 620: [Real subtraction reverses addition, 2] ((X in Re) & (Y in Re)) •imp (X = (Y •R_PLUS (X •R_MINUS Y)))
(786) Theorem 636: [Distributivity of division over addition] ((X in Re) & (Y in Re) & (V in Re) & (V /= R_0)) •imp ((X •R_PLUS Y) •R_OVER V = ((X •R_OVER V) •R_PLUS (Y •R_OVER V)))
(796) Theorem 646: [The sum and product of two non-negative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (R_is_nonneg(X •R_PLUS Y) & R_is_nonneg(X •R_TIMES Y))
(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))
(818) Theorem 668: [Monotonicity of addition over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (XP •R_GE YP)) •imp ((X •R_PLUS XP) •R_GE (X •R_PLUS YP))
(819) Theorem 669: [Monotonicity of addition] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (XP •R_GE YP)) •imp ((X •R_PLUS XP) •R_GE (Y •R_PLUS YP))
(820) Theorem 670: [Strict monotonicity of addition] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (XP •R_GT YP)) •imp ((X •R_PLUS XP) •R_GT (Y •R_PLUS YP))
(821) Theorem 671: [Strict monotonicity of addition, 2] ((X in Re) & (Y in Re) & (V in Re) & (X •R_GE Y)) •imp (((Y •R_PLUS V) •R_GE (X •R_PLUS V)) •eq (X = Y))
(822) Theorem 672a: ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_PLUS Y = R_0)) •imp ((X = R_0) & (Y = R_0))
(833) Theorem 682: [The sum of non-negative reals is at least as big at each addend] ((X in Re) & (Y in Re) & (X •R_GE R_0)) •imp ((X •R_PLUS Y) •R_GE Y)
(838) Theorem 685: [Properties of the real number 2] ((R_1 •R_PLUS R_1) in Re) & ((R_1 •R_PLUS R_1) •R_GT R_0) & (R_Recip(R_1 •R_PLUS R_1) in Re) & (R_Recip(R_1 •R_PLUS R_1) /= R_0) & ((X in Re) •imp ((X •R_OVER (R_1 •R_PLUS R_1)) in Re))
(839) Theorem 686: [Any real number can be divided into two equal halves] (X in Re) •imp (X = (X •R_OVER (R_1 •R_PLUS R_1)) •R_PLUS (X •R_OVER (R_1 •R_PLUS R_1)))
(840) Theorem 687: [The average of two real numbers lies between them] ((X in Re) & (Y in Re) & (X •R_GT Y)) •imp ((X •R_GT ((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1))) & (((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) •R_GT Y))
(841) Theorem 688: [Every positive real exceeds the sum of two smaller positive reals] ((X in Re) & (X •R_GT R_0)) •imp (EXISTS E in Re , E0 in Re | (X •R_GT E) & (E •R_GT E0) & (E0 •R_GT R_0) & (E •R_GT R_0) & (X •R_GT (E •R_PLUS E0)))
(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)))
(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)))
(852) Theorem 699: ((X in Re) & (Y in Re)) •imp (((X •R_PLUS abs(Y)) •R_GE X))
(853) Theorem 700: ((X in Re) & (Y in Re)) •imp (((abs(X) •R_PLUS abs(Y)) •R_GT abs(X •R_PLUS Y)) or ((abs(X) •R_PLUS abs(Y)) = abs(X •R_PLUS Y)))
(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)))
(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))))
(879) Theorem 724: [The limit of a sum is the sum of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_PLUS G) = (limit(F) •R_PLUS limit(G)))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))
(902) Theorem 747: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re)) & (X in Re)) •imp (((Polval(F,X) •R_PLUS Polval(G,X)) = Polval(F •PolPlus G,X)) & ((Polval(F,X) •R_MINUS Polval(G,X)) = Polval(F •PolMinus G,X)) & ((Polval(F,X) •R_TIMES Polval(G,X)) = Polval(F •PolTimes G,X)))
(919) Theorem 763a: [The square of the square root of any real w=(x •R_TIMES x) •R_PLUS (y •R_TIMES y) is w] ((X in Re) & (Y in Re)) •imp (sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) •R_TIMES sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) = ((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)))
(921) Theorem 20001: ((N in Re) & (M in Re)) •imp (((abs(N) •R_PLUS abs(M)) •R_GT abs(N •R_MINUS M)) or ((abs(N) •R_PLUS abs(M)) = abs(N •R_MINUS M)))
(922) Theorem 20003: ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_PLUS Y = R_0)) •imp ((X = R_0) & (Y = R_0))
(924) Theorem 20005: ((X in Re) & (Y in Re) & (X •R_GT Y)) •imp (X •R_GT ((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) & (((X •R_PLUS Y) •R_OVER (R_1 •R_PLUS R_1)) •R_GT Y))
(937) Theorem 814: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_PLUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_PLUS M)))
(938) Theorem 815: ((N in Cm) & (M in Cm)) •imp (((C_abs(N) •R_PLUS C_abs(M)) •R_GT C_abs(N •C_MINUS M)) or (C_abs(N) •R_PLUS C_abs(M) = C_abs(N •C_MINUS M)))
(947) Theorem real_sigma0: (FORALL f | (Finite(f) & (range(f) •incin Re)) •imp (Sig(f) in Re)) & (FORALL x | (cdr(x) in Re) •imp (Sig({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (Sig(f) = (Sig(f •ON (domain(f) * t)) •R_PLUS Sig(f •ON (domain(f) - t)))))
(948) Theorem real_sigma: (Svm(F) & (range(F) •incin Re) & Finite(F)) •imp ((Sig(F) in Re) & ((P in F) •imp (Sig({P}) = (F~[car(P)]))) & (Sig(F) = (Sig(F •ON (domain(F) * A)) •R_PLUS Sig(F •ON (domain(F) - A)))))
(955) Theorem real_function_sigma: (Svm(ser) & (range(ser) •incin RF) & Finite(ser)) •imp ((FSig(ser) in RF & (p in ser) •imp (Sig({p}) = ser(car(p)))) &(FORALL a | Sig(ser) = Sig(ser •ON (domain(ser) * a)) •R_PLUS Sig(ser •ON domain(ser) - a)))
(957) Theorem 20013: [Cauchy integral formula] (is_analytic_CF(f) & (domain(f) incs {w in Cm | C_abs(w) •R_GE R_1})) •imp (FORALL w in Cm | (C_abs(w) •R_GT R_1) •imp ((f~[w]) = (Line_Int({[x,(f~[x]) •C_OVER (x •C_MINUS w)]: x in (Cm -{w})}, {[x,C_exp_fcn([R_0,x])]: x in Re}, R_0, pi •R_PLUS pi) •C_OVER ([R_0,pi •R_PLUS pi])) ))