List of theorems referencing the symbol RE

(739) Theorem 588: (FORALL x, y | ((x in RaCauchy) & (y in RaCauchy)) •imp ((Ra_eqseq(x,y) •eq (Cauchy_to_Re(x) = Cauchy_to_Re(y))))) & (FORALL x | (x in Re) •imp ((arb(x) in RaCauchy) & (Cauchy_to_Re(arb(x)) = x))) & (FORALL x | (x in RaCauchy) •imp (Cauchy_to_Re(x) in Re)) & (FORALL x | (x in RaCauchy) •imp Ra_eqseq(x,arb(Cauchy_to_Re(x))))
(740) Theorem 589: ((X in RaCauchy) & (Y in RaCauchy)) •imp ((Ra_eqseq(X,Y) •eq (Cauchy_to_Re(X) = Cauchy_to_Re(Y))) & (Cauchy_to_Re(X) in Re) & Ra_eqseq(X,arb(Cauchy_to_Re(X))))
(741) Theorem 590: (X in Re) •imp ((arb(X) in RaCauchy) & (arb(X) in RaSeq) & (Cauchy_to_Re(arb(X)) = X))
(742) Theorem 591: (R_0 in Re) & (R_1 in Re)
(743) Theorem 592: ({X,Y} •incin Re) •imp (((X •R_PLUS Y) in Re) & (R_Rev(X) in Re))
(744) Theorem 593: ({X,Y} •incin Re) •imp (((X •R_MINUS Y) in Re) & ((X •R_TIMES Y) in Re))
(745) Theorem 594: [Commutative law for real addition] ({X,Y} •incin Re) •imp ((X •R_PLUS Y) = (Y •R_PLUS X))
(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))
(748) Theorem 597: [Commutative law for real multiplication] ({X,Y} •incin Re) •imp ((X •R_TIMES Y) = (Y •R_TIMES X))
(750) Theorem 599: [Associative law for real multiplication] ({X,Y,V} •incin Re) •imp ((X •R_TIMES (Y •R_TIMES V)) = ((X •R_TIMES Y) •R_TIMES 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)))
(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)))
(754) Theorem 603: [Any real times 0 is 0] (X in Re) •imp ((X •R_TIMES R_0) = R_0)
(755) Theorem 604: [0 times any real is 0] (X in Re) •imp (R_0 •R_TIMES X = R_0)
(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))
(757) Theorem 606: [1 is a right multiplicative identity for reals] (X in Re) •imp (X •R_TIMES R_1 = X)
(758) Theorem 607: [1 is a left multiplicative identity for reals] (X in Re) •imp (R_1 •R_TIMES X = X)
(760) Theorem 609: [0 is right identity for real subtraction] (X in Re) •imp (X •R_MINUS R_0 = X)
(761) Theorem 610: [Real subtraction principle] (X in Re) •imp (X •R_MINUS X = 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)
(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))
(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))
(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)))
(771) Theorem 621: [Multiplication by R_Rev(R_1)] (X in Re) •imp (R_Rev(X) = R_Rev(R_1) •R_TIMES X)
(772) Theorem 622: [Distributivity of multiplication over subtraction] ((X in Re) & (Y in Re) & (V in Re)) •imp ((X •R_TIMES (Y •R_MINUS V)) = ((X •R_TIMES Y) •R_MINUS (X •R_TIMES V)))
(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))
(774) Theorem 624: [Real reciprocal principle] ((X in Re) & (X /= R_0)) •imp (X •R_TIMES R_Recip(X) = R_1)
(775) Theorem 625: [Real division principle] ((X in Re) & (X /= R_0)) •imp (X •R_OVER X = R_1)
(776) Theorem 626: [Basic properties of the reciprocal for reals] ((X in Re) & (X /= R_0)) •imp ((R_Recip(X) in Re) & (R_Recip(X) /= R_0) & ((R_Recip(X) •R_TIMES X) = R_1))
(777) Theorem 627: [Basic properties of the reciprocal for reals, 2] ((X in Re) & (X /= R_0)) •imp (R_Recip(R_Recip(X)) = 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)))
(779) Theorem 629: [Real multiplicative Cancellation] ((X in Re) & (Y in Re) & (V in Re) & (X •R_TIMES V = Y •R_TIMES V) & (V /= R_0)) •imp (X = Y)
(780) Theorem 630: [Reals are closed under division] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y in Re) & ((X /= R_0) •imp ((X •R_OVER Y /= R_0) & (X •R_TIMES Y /= R_0))))
(781) Theorem 631: [Real division is multiplication by the reciprocal] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_OVER Y) = (X •R_TIMES R_Recip(Y)))
(782) Theorem 632: [The reciprocal of a real product is the product of the reciprocals] ((X in Re) & (Y in Re) & (X /= R_0) & (Y /= R_0)) •imp ((X •R_TIMES Y /= R_0) & R_Recip(X •R_TIMES Y) = R_Recip(X) •R_TIMES R_Recip(Y))
(783) Theorem 633: [Real multiplication-division commutativity] ((X in Re) & (Y in Re) & (Y /= R_0) & (V in Re) & (V /= R_0)) •imp (X •R_OVER (Y •R_TIMES V) = (X •R_OVER Y) •R_OVER V)
(784) Theorem 634: [A real divided by itself gives 1] ((X in Re) & (X /= R_0)) •imp (X •R_OVER X = R_1)
(785) Theorem 635: [Real reciprocal as a quotient] ((X in Re) & (X /= R_0)) •imp (R_Recip(X) = R_1 •R_OVER X)
(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)))
(787) Theorem 637: [Real division reverses multiplication] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((X •R_TIMES Y) •R_OVER Y = X)
(788) Theorem 638: [Real division reverses multiplication,2] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp (X = (Y •R_TIMES (X •R_OVER Y)))
(789) Theorem 639: [Distributivity of division over subtraction] ((X in Re) & (Y in Re) & (V in Re) & (V /= R_0)) •imp (((X •R_MINUS Y) •R_OVER V) = ((X •R_OVER V) •R_MINUS (Y •R_OVER V)))
(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))))))
(791) Theorem 641: ((X in Re) & (Y in Re)) •imp Ra_eqseq((arb(X) •Ras_PLUS arb(Y)),arb(Cauchy_to_Re(arb(X) •Ras_PLUS arb(Y))))
(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)))
(793) Theorem 643: [Each non-negative rational Cauchy sequences is equivalent to its own absolute value] (X in Re) •imp (R_is_nonneg(X) •eq Ra_eqseq(arb(X),Ras_ABS(arb(X))))
(794) Theorem 644: [The sum of two non-negative rational Cauchy sequences is equivalent to its own absolute value] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp Ra_eqseq(arb(X) •Ras_PLUS arb(Y),Ras_ABS(arb(X) •Ras_PLUS arb(Y)))
(795) Theorem 645: [The product of two non-negative rational Cauchy sequences is equivalent to its own absolute value] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp Ra_eqseq(arb(X) •Ras_TIMES arb(Y),Ras_ABS(arb(X) •Ras_TIMES arb(Y)))
(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))
(797) Theorem 647: [Transitivity of ordering] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GE Y) & (Y •R_GE Z)) •imp (X •R_GE Z)
(798) Theorem 648: [The reals are a linearly ordered set] ((X in Re) & (Y in Re)) •imp ((X •R_GT Y) or (X = Y) or (Y •R_GT X))
(799) Theorem 649: [The reals are a linearly ordered set, 2] ((X in Re) & (Y in Re)) •imp ((X •R_LT Y) or (X = Y) or (Y •R_LT X))
(801) Theorem 651: [The reals are a linearly ordered set, 3] ((X in Re) & (Y in Re)) •imp (((X •R_GE Y) or (Y •R_GE X)) & (((X •R_GE Y) & (Y •R_GE X)) •imp (X = 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))
(805) Theorem 655: [Transitivity of ordering, strict case] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Y •R_GE Z)) •imp (X •R_GT Z)
(806) Theorem 656: [Transitivity of ordering, strict case 2] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GE Y) & (Y •R_GT Z)) •imp (X •R_GT Z)
(807) Theorem 657: [Transitivity of ordering,strict case 3] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Y •R_GT Z)) •imp (X •R_GT Z)
(808) Theorem 658: [Greater_than_equal is greater-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_GE Y) •eq ((X •R_GT Y) or (X = Y)))
(809) Theorem 659: [Greater_than_equal is greater-than and equal] (X in Re) •imp ((X •R_GE R_0) •eq R_is_nonneg(X))
(810) Theorem 660: [Less_than_equal is less-than and equal] ((X in Re) & (Y in Re)) •imp ((X •R_LE Y) •eq ((X •R_LT Y) or (X = Y)))
(811) Theorem 661: [Transitivity of ordering by 'less than'] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LE Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(812) Theorem 662: [Transitivity of ordering by 'less than', 2] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LE Z)) •imp (X •R_LT Z))
(813) Theorem 663: [Transitivity of ordering by 'less than', 3] ((X in Re) & (Y in Re) & (Z in Re)) •imp (((X •R_LT Y) & (Y •R_LT Z)) •imp (X •R_LT Z))
(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))))
(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))
(823) Theorem 672: [The product of two reals is 0 if and only if one of them is 0] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) = R_0) •eq ((X = R_0) or (Y = R_0)))
(824) Theorem 673: [Monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (X •R_TIMES YP))
(825) Theorem 674: [Monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GE R_0) & (YP •R_GE R_0) & (XP •R_GE YP)) •imp ((X •R_TIMES XP) •R_GE (Y •R_TIMES YP))
(826) Theorem 675: [Strict monotonicity of multiplication over 2nd argument] ((X in Re) & (XP in Re) & (YP in Re) & (X •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (X •R_TIMES YP))
(827) Theorem 676: [Strict monotonicity of multiplication] ((X in Re) & (Y in Re) & (XP in Re) & (YP in Re) & (X •R_GE Y) & (Y •R_GT R_0) & (YP •R_GT R_0) & (XP •R_GT YP)) •imp ((X •R_TIMES XP) •R_GT (Y •R_TIMES YP))
(828) Theorem 677: [Multiplication by a positive real is strictly monotone] ((X in Re) & (Y in Re) & (Z in Re) & (X •R_GT Y) & (Z •R_GT R_0)) •imp ((X •R_TIMES Z) •R_GT (Y •R_TIMES Z))
(829) Theorem 678: [The product of reals x,y of which x is positive is non-negative iff y is non-negative] ((X in Re) & (Y in Re) & (X /= R_0) & R_is_nonneg(X)) •imp (R_is_nonneg(X •R_TIMES Y) •eq R_is_nonneg(Y))
(830) Theorem 679: [The product of nonnegative reals is non-negative] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp R_is_nonneg(X •R_TIMES Y)
(831) Theorem 680: [Condition for positiveness of a product of reals] ((X in Re) & (Y in Re)) •imp (((X •R_TIMES Y) •R_GT R_0) •eq (((X •R_GT R_0) & (Y •R_GT R_0)) or ((R_0 •R_GT X) & (R_0 •R_GT Y))))
(832) Theorem 681: [The reciprocal of a positive real is positive] ((X in Re) & (X •R_GT R_0)) •imp (R_Recip(X) •R_GT 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)
(834) Theorem 683: [The reciprocal is monotone decreasing for positive reals] ((X in Re) & (Y in Re) & (X •R_GT Y) & (Y •R_GT R_0)) •imp (R_Recip(Y) •R_GT R_Recip(X))
(835) Theorem 683a: [Two non-null reals are equal iff their reciprocals are equal] ((X in Re) & (X /= R_0) & (Y in Re) & (Y /= R_0) & (R_Recip(X) = R_Recip(Y))) •imp (X = Y)
(836) Theorem 684: [The square of any real is non-negative] (X in Re) •imp R_is_nonneg(X •R_TIMES X)
(837) Theorem 684a: [Monotonicity of squaring] ((X in Re) & (Y in Re) & (X •R_GE R_0) & (Y •R_GE R_0)) •imp ((X •R_GE Y) •eq ((X •R_TIMES X) •R_GE (Y •R_TIMES 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)))
(842) Theorem 689: [Every positive real exceeds some smaller positive real] ((X in Re) & (X •R_GT R_0)) •imp (EXISTS E in Re | (X •R_GT E) & (E •R_GT R_0))
(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)))
(845) Theorem 692: [The absolute value of x is a non-negative real no smaller than x] (X in Re) •imp ((abs(X) in Re) & (abs(X) •R_GE R_0) & (abs(X) •R_GE X) & (R_is_nonneg(abs(X))))
(846) Theorem 693: [The absolute value of x is whichever of x and -x is non-negative] (X in Re) •imp (abs(X) = if R_is_nonneg(X) then X else R_Rev(X) end if)
(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)
(848) Theorem 695: [The absolute value of a real product is the product of absolute values] ((X in Re) & (Y in Re)) •imp (abs(X •R_TIMES Y) = (abs(X) •R_TIMES abs(Y)))
(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)))
(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)))
(854) Theorem 701: [The absolute value of a real quotient is the quotient of absolute values] ((X in Re) & (Y in Re) & (Y /= R_0)) •imp ((abs(X) •R_OVER abs(Y)) = abs(X •R_OVER 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))))
(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)))
(864) Theorem 710a: [The images of rationals via the embedding form a dense subset of the reals, 1] ((X in Re) & (Eps in Ra) & (Eps •Ra_GT Ra_0)) •imp (EXISTS y in Ra | Finite({m in Za | Ra_ABS(((arb(X))~[m]) •Ra_MINUS y) •Ra_GE Eps}) )
(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))))
(876) Theorem 722b: [Every real Cauchy sequence has a real limit] (F in ReCauchy) •imp ((Ra_approx(F) in RaCauchy) & (Ra_approx(F) in RaSeq) & Ra_apseq(F,Ra_approx(F)) & (limit(F) in Re))
(883) Theorem 728: [Any real x is included between two rationals which can be arbitrarily close together] ((X in Re) & (EPS in Re) & (EPS •R_GT R_0)) •imp (EXISTS r1 in Ra, r2 in Ra | ((ReRa(r1) •R_GT X) & (X •R_GT ReRa(r2)) & (ReRa(r1 •Ra_MINUS r2) •R_LE EPS)))
(884) Theorem 729: [For any real x, there exists a rational r such that r >= x] (x in Re) •imp (EXISTS r in Ra | ReRa(r) •R_GT x)
(887) Theorem 732: [For any real x, there exists an integer n such that n > x] (x in Re) •imp (EXISTS n in Za | ReRa(RaSi(SiZa(n))) •R_GT x)
(888) Theorem 733: [For any real x and eps > 0, there exists an integer n such that n • eps > x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | ((ReRa(RaSi(SiZa(n))) •R_TIMES e) •R_GT x))
(889) Theorem 734: [For any real x and eps > 0, there exists an integer n such that eps > x/n] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (eps •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(890) Theorem 735: [For any non-negative real x and eps > 0, there exists an integer n such that n •R_TIMES eps > x and (n - 1) • eps <= x] ((x in Re) & (eps in Re) & (eps •R_GT R_0)) •imp (EXISTS n in Za | (e •R_GT (x •R_OVER ReRa(RaSi(SiZa(n))))))
(891) Theorem 736: [Every positive real is bounded below by a rational fraction of the form 1/n] ((x in Re) & (x •R_GT R_0)) •imp (EXISTS n in Za | (R_1 •R_OVER ReRa(RaSi(SiZa(n)))) •R_LT x)
(894) Theorem 739: [For any non-empty set s of reals which is bounded above, and for any positive real eps, there exists an u in s such that u + eps is an upper bound of s] ((s •incin Re) & (s /= 0) & (eps in Re) & (eps •R_GT R_0) & (y in Re) & (FORALL x in s | y •R_GE x)) •imp (EXISTS u in s | (FORALL x in s | u •R_GE x))
(895) Theorem 740: [Any bounded set of reals has a least upper bound] ((S •incin Re) & (S /= 0) & (EXISTS y in Re | (FORALL x in s | y •R_GE x))) •imp (EXISTS u in Re | ((FORALL x in s | u •R_GE x) & (FORALL v in Re | (v •R_LT u •imp (not (FORALL x in s | v •R_GE x))))))
(897) Theorem 742: ((N in Za) & (X in Re)) •imp (X •ToThe N = if (N = 0) then R_1 else X •R_TIMES (X •ToThe (N - 1)) end if)
(898) Theorem 743: (X in Re) •imp ((X •ToThe 0 = R_0) & (X •ToThe 1 = X) & (((M in Za) & (N in Za)) •imp (X •ToThe (M •PLUS N) = (X •ToThe M) •R_TIMES (X •ToThe N))))
(899) Theorem 744: ((X in Re) & (M in Za) & (N in Za)) •imp (((X •ToThe M) •ToThe N) = (X •ToThe (M •TIMES N)))
(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)))
(903) Theorem 748: ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp (((PolFcn(F) •F_PLUS PolFcn(G)) = PolFcn(F •PolPlus G)) & ((PolFcn(F) •F_MINUS PolFcn(G)) = PolFcn(F •PolMinus G)) & ((PolFcn(F) •F_TIMES PolFcn(G)) = PolFcn(F •PolTimes G)))
(908) Theorem 753: [Polynomial functions are continuous everywhere] (F in Fin_Seqs(Re)) •imp Cf_RR(PolFcn(F),Re)
(909) Theorem 754: [Polynomial quotients are continuous wherever their denominator is nonzero] ((F in Fin_Seqs(Re)) & (G in Fin_Seqs(Re))) •imp Cf_RR(F •F_OVER G,{x in Re | G~[x] /= R_0})
(910) Theorem 755: [Crossing-completness principle for the real numbers] ((Cf_RR(F,I(X,Y)) & (X in Re) & (Y in Re) & (R_0 •R_GE F~[X]) & (R_0 •R_LE F~[Y]) & (X •R_LE Y)) •imp (EXISTS v | ((X •R_LE V) & (V •R_LE Y) & (F~[v] = R_0))))
(913) Theorem 758: (Cf_RR(F,I(X,Y)) & (X in Re) & (Y in Re)) •imp (EXISTS u in I(X,Y), v in I(X,Y) | range(F •ON I(X,Y)) = I(f~[u],f~[v]))
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))
(915) Theorem 760: [The square of the square root of any positive x is x] ((X in Re) & (R_is_nonneg(X))) •imp ((sqrt(X) in Re) & (R_is_nonneg(sqrt(X))) & ((sqrt(X) •R_TIMES sqrt(X)) = X))
(916) Theorem 761: [The positive square root is unique] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & ((Y •R_TIMES Y) = X)) •imp (Y = sqrt(X))
(917) Theorem 762: [The square root is monotone increasing for positive numbers] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_GT Y)) •imp (sqrt(X) •R_GT sqrt(Y))
(918) Theorem 763: [The square root of a product is the product of the square roots] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (sqrt(X •R_TIMES Y) = (sqrt(X) •R_TIMES sqrt(Y)))
(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)))
(921+) Theorem 20002: ((N in Re) & (M in Re) & (M /= R_0)) •imp (abs(N) •R_OVER abs(M) = abs(N •R_OVER 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))
(923) Theorem 20004: ((X in Re) & (Y in Re) & (X1 in Re) & (X •R_GT Y) & (X1 •R_GT R_0)) •imp ((X •R_TIMES X1) •R_GT (Y •R_TIMES X1))
(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))
(925) Theorem 804a: ((X in Re) & (Y in Re)) •imp ([X,Y] in Cm)
(926) Theorem 804: (M in Cm) •eq ((M = [car(M),cdr(M)]) & (car(M) in Re) & (cdr(M) in Re))
(935) Theorem 812: (N in Cm) •imp ((C_abs(N) in Re) & R_is_nonneg(C_abs(N)))
(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)))))
(956) Theorem 20012: [Cauchy integral theorem] is_analytic_CF(f) •imp (EXISTS eps in Re | (eps •R_GT R_0) & (FORALL crv1, crv2 | (is_CD_curv(crv1,R_0,R_1) & is_CD_curv(crv2,R_0,R_1) & ((crv1~[R_0]) = (crv1~[R_1])) & ((crv2~[R_0]) = (crv2~[R_1])) & (FORALL x in Interval(R_0,R_1) | eps •R_GE C_abs((crv1~[x]) •C_MINUS (crv2~[x])))) •imp (Line_Int(f,crv1,R_0,R_1) = Line_Int(f,crv2,R_0,R_1)) ))
(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])) ))