List of theorems referencing the symbol RA_EQSEQ

(668) Theorem 522: [Reformulation of condition for sequence equivalence] ({F,G} •incin RaSeq) •imp (Ra_eqseq(F,G) •eq (FORALL eps in Ra | (eps •Ra_GT Ra_0) •imp Finite({x : x in Za | Ra_ABS((F~[x]) •Ra_MINUS (G~[x])) •Ra_GT eps})))
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(681) Theorem 530: ((F in RaCauchy) & (G in Subseqs(F)) & (not Finite(G))) •imp ((G in RaCauchy) & Ra_eqseq(F,G))
(685) Theorem 534: (({F,G,H} •incin RaSeq) & Ra_eqseq(F,G) & Ra_eqseq(G,H)) •imp Ra_eqseq(H,F)
(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))
(703) Theorem 552: (({F,G,Fp,Gp} •incin RaSeq) & Ra_eqseq(F,G) & Ra_eqseq(Fp,Gp)) •imp Ra_eqseq(F •Ras_PLUS Fp, G •Ras_PLUS Gp)
(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)))
(733) Theorem 582: [The unit Cauchy sequences Ra0Seq,Ra1Seq differ from one another] (not Ra_eqseq(Ra0Seq,Ra1Seq))
(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))))
(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))))
(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)))
(855) Theorem 702: (X in Ra) •imp (Ra_is_nonneg(X) •eq Ra_eqseq(Za •PROD {Ra_ABS(X)},Za •PROD {X}))