List of theorems referencing the symbol RACAUCHY

(666) Theorem 520: [Every Rational Cauchy sequence is a rational sequence] RaCauchy •incin RaSeq
(675) Theorem 524: (X in Ra) •imp ((Za •PROD {X}) in RaCauchy)
(677) Theorem 526: {Ra0Seq,Ra1Seq} •incin RaCauchy
(681) Theorem 530: ((F in RaCauchy) & (G in Subseqs(F)) & (not Finite(G))) •imp ((G in RaCauchy) & Ra_eqseq(F,G))
(682) Theorem 531: (F in RaCauchy) •imp ((H in Za) •imp (F~[H] in Ra))
(683) Theorem 532: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (not (Ra_ABS((F~[i]) •Ra_MINUS (F~[j]))) •Ra_GT Eps)))
(684) Theorem 533: ((Eps in Ra) & (Eps •Ra_GT Ra_0) & (F in RaCauchy)) •imp (EXISTS k in Za | (FORALL i in Za, j in Za | ((i notin k) & (j notin k)) •imp (Eps •Ra_GT (Ra_ABS((F~[i]) •Ra_MINUS (F~[j])))) ))
(688) Theorem 537: ({F,G} •incin RaCauchy) •imp (((F •Ras_PLUS G) in RaCauchy) & (Ras_ABS(F) in RaCauchy) & (Ras_Rev(F) in RaCauchy))
(691) Theorem 540: [Every Cauchy sequence has an upper bound] (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | y •Ra_LE x))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_LT x ))
(693) Theorem 542: ({F,G} •incin RaCauchy) •imp (((F •Ras_MINUS G) in RaCauchy) & ((F •Ras_TIMES G) in RaCauchy))
(694) Theorem 543: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra | (eps •Ra_GT Ra_0) & Finite({i in Za | eps •Ra_GE Ra_ABS(G~[i])}))
(695) Theorem 544: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(G~[i]) •Ra_GT eps) & (Ra_ABS(G~[i]) •Ra_GT Ra_0)) & (Ra_ABS(G~[n]) •Ra_GT Ra_0))
(696) Theorem 545: ((H in RaCauchy) & (not Ra_eqseq(H,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | Ra_ABS(H~[i]) •Ra_GT eps) & (FORALL i in Za, j in Za | ((i notin n) & (j notin n)) •imp (eps •Ra_GT (Ra_ABS((H~[i]) •Ra_MINUS (H~[j]))))))
(697) Theorem 546: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ({h in Za | (FORALL i in (Za - h) | (G~[i]) /= Ra_0)} /= 0)
(699) Theorem 548: ((F in RaCauchy) & (M in Za)) •imp ((shifted_seq(F,M) in RaCauchy) & Ra_eqseq(F,shifted_seq(F,M)))
(700) Theorem 549: ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS g in RaCauchy | Ra_eqseq(F,g) & (Ras_Recip(F) = Ras_Recip(g)) & (FORALL i in Za | ((g~[i]) /= Ra_0) & (Ras_Recip(g)~[i] = Recip(g~[i]))))
(701) Theorem 550: [The reciprocal of a non-null rational sequence is a rational sequence] ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (Ras_Recip(G) in RaSeq)
(702) Theorem 551: [Reciprocal and quotient of rational Cauchy sequences are, when defined, Cauchy sequences] (({F,G} •incin RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ((Ras_Recip(G) in RaCauchy) & ((F •Ras_OVER G) in RaCauchy))
(704) Theorem 553: (({F,G,Fp,Gp} •incin RaCauchy) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_PLUS Fp, G •Ras_PLUS Gp)
(705) Theorem 554: (({F,Fp,G} •incin RaCauchy) & Ra_eqseq(F,Fp)) •imp Ra_eqseq(F •Ras_TIMES G, Fp •Ras_TIMES G)
(706) Theorem 555: (({F,G,Fp,Gp} •incin RaCauchy) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_TIMES Fp, G •Ras_TIMES Gp)
(707) Theorem 556: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_Rev(F),Ras_Rev(G))
(708) Theorem 557: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_ABS(F),Ras_ABS(G))
(709) Theorem 558: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G) & (not(Ra_eqseq(F,Ra0Seq)))) •imp Ra_eqseq(Ras_Recip(F),Ras_Recip(G))
(723) Theorem 572: [Reciprocal sequence principle] ((X in RaCauchy) & (not Ra_eqseq(X,Ra0Seq))) •imp Ra_eqseq(X •Ras_TIMES Ras_Recip(X),Ra1Seq)
(729) Theorem 578: [?] ((H in RaCauchy) & Ra_eqseq(H,Ra0Seq)) •imp (Ra_eqseq(Ras_ABS(H),Ra0Seq) & (Ra_eqseq(Ras_Rev(H),Ra0Seq)))
(730) Theorem 579: [All terms of a Cauchy sequence not equivalent to zero have the same sign and have an absolute value bounded below beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS eps in Ra, n in Za | (eps •Ra_GT Ra_0) & (FORALL i in (Za - n) | (Ra_ABS(F~[i]) •Ra_GT eps) & (Ra_ABS(F~[i]) = if ((F~[n]) •Ra_GE Ra_0) then (F~[i]) else Ra_Rev(F~[i]) end if) ))
(731) Theorem 580: [All terms of a Cauchy sequence not equivalent to zero have the same sign beyond a certain point] ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS n in Za | shifted_seq(Ras_ABS(F),n) = if ((F~[n]) •Ra_GE Ra_0) then shifted_seq(F,n) else shifted_seq(Ras_Rev(F),n) end if)
(732) Theorem 581: [One of a Cauchy sequence F and its additive inverse is always equivalent to a non-negative sequence, and both are equivalent to non-negative sequences only if F is equivalent to zero] (F in RaCauchy) •imp (((Ra_eqseq(Ras_ABS(F),F) or Ra_eqseq(Ras_ABS(F),Ras_Rev(F)))) & (((Ra_eqseq(Ras_ABS(F),F) & Ra_eqseq(Ras_ABS(F),Ras_Rev(F)))) •imp Ra_eqseq(F,Ra0Seq)))
(736) Theorem 585: (FORALL f in RaCauchy, g in RaCauchy | (Ra_eqseq(f,g) •eq Ra_eqseq(g,f)) & Ra_eqseq(f,f))
(737) Theorem 586: ((F in RaCauchy) & (G in RaCauchy)) •imp ((Ra_eqseq(F,G) •eq Ra_eqseq(G,F)) & Ra_eqseq(F,F))
(738) Theorem 587: (FORALL f in RaCauchy, g in RaCauchy, h in RaCauchy | (Ra_eqseq(f,g) & Ra_eqseq(g,h)) •imp Ra_eqseq(f,h))
(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)))
(875) Theorem 722a: [Every real Cauchy sequence can be approximated by a rational sequence] (F in ReCauchy) •imp (Ra_approx(F) in {g in RaCauchy | Ra_apseq(F,g)})
(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))
(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)))
(878) Theorem 723: [The elementary operations on reals map Cauchy sequences into Cauchy sequences] ((F in ReCauchy) & (G in ReCauchy) & (Fp in RaCauchy) & (Gp in RaCauchy) & Ra_apseq(F,Fp) & Ra_apseq(G,Gp)) •imp ((((F •Res_PLUS G in ReCauchy) & Ra_apseq(F •Res_PLUS G,Fp •Ras_PLUS Gp))) & (((F •Res_MINUS G in ReCauchy) & Ra_apseq(F •Res_MINUS G,Fp •Ras_MINUS Gp))) & (((F •Res_TIMES G in ReCauchy) & Ra_apseq(F •Res_TIMES G,Fp •Ras_TIMES Gp))))
(892) Theorem 737: [Every real Cauchy sequence is approximated by a rational Cauchy sequence] (F in ReCauchy) •imp (EXISTS g in RaCauchy | Ra_apseq(F,g))
(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)))