List of theorems referencing the symbol R_1
(742) Theorem 591: (R_0 in Re) & (R_1 in Re)
(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)
(771) Theorem 621: [Multiplication by R_Rev(R_1)] (X in Re) •imp (R_Rev(X) = R_Rev(R_1) •R_TIMES 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))
(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)
(800) Theorem 650: [0 and 1 are non-negative reals] R_is_nonneg(R_0) & R_is_nonneg(R_1)
(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)
(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))
(861) Theorem 708: [The embedding of rationals into reals preserves 0 and 1] (ReRa(Ra_0) = R_0) & (ReRa(Ra_1) = R_1)
(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)
(896) Theorem 741: (FORALL s, x | (Finite(s) •imp (ToThe1(s,x) = if (s = 0) then R_1 else ToThe1(s - {arb(s)},x) •R_TIMES x end if)))
(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)
(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))
(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])) ))