List of theorems referencing the symbol CAUCHY_TO_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))
(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)))
(749) Theorem 598: [Elementary algebraic lemma for real multiplication] ((X in RaCauchy) & (Y in RaCauchy)) •imp (Cauchy_to_Re(X •Ras_TIMES Y) = (Cauchy_to_Re(X) •R_TIMES Cauchy_to_Re(Y)))
(752) Theorem 601: [Lemma for law of signs] (X in RaCauchy) •imp (Cauchy_to_Re(Ras_Rev(X)) = R_Rev(Cauchy_to_Re(X)))
(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))))
(856) Theorem 703: (X in Ra) •imp (R_is_nonneg(Cauchy_to_Re(Za •PROD {X})) •eq (ReRa(Ra_ABS(X)) = ReRa(X)))
(877) Theorem 722: [The limit of a real Cauchy sequence is the real defined by any of its rational approximations] ((F in ReCauchy) & (G in RaSeq) & Ra_apseq(F,G)) •imp ((G in RaCauchy) & (Cauchy_to_Re(G) = limit(F)))
(893) Theorem 738: [Any two approximating rational sequences for a given real Cauchy sequence are equivalent] ((F in ReCauchy) & Ra_apseq(F,G) & Ra_apseq(F,GP)) •imp ((G in RaCauchy) & (GP in RaCauchy) & (Cauchy_to_Re(G) = Cauchy_to_Re(GP)))