List of theorems referencing the symbol RASEQ

(666) Theorem 520: [Every Rational Cauchy sequence is a rational sequence] RaCauchy •incin RaSeq
(667) Theorem 521: [The range of a rational sequence is included in the set of rationals] (F in RaSeq) •imp ((domain(F) = Za) & (range(F) •incin Ra) & ((X in Za) •imp (F~[X] in Ra)))
(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})))
(669) Theorem 523: [Condition for rational sequence equality] (FORALL n in Za | ((F in RaSeq) & (G in RaSeq) & (F~[n] = G~[n]))) •imp (F = G)
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(679) Theorem 528: ((F in RaSeq) & (N in Za) & (I in Za)) •imp ((shifted_seq(F,N)~[I]) = (F~[N •PLUS I]))
(685) Theorem 534: (({F,G,H} •incin RaSeq) & Ra_eqseq(F,G) & Ra_eqseq(G,H)) •imp Ra_eqseq(H,F)
(686) Theorem 535: ({F,G} •incin RaSeq) •imp (((F •Ras_PLUS G) in RaSeq) & (Ras_ABS(G) in RaSeq) & (Ras_Rev(G) in RaSeq) & ((F •Ras_TIMES G) in RaSeq) & ((F •Ras_PLUS G) = {[u,((F~[u]) •Ra_PLUS (G~[u]))]: u in Za}) & (Ras_ABS(G) = {[u,Ra_ABS(G~[u])]: u in Za}) & (Ras_Rev(G) = {[u,Ra_Rev(G~[u])]: u in Za}) & ((F •Ras_TIMES G) = {[u,((F~[u]) •Ra_TIMES (G~[u]))]: u in Za}))
(687) Theorem 536: (({F1,G1} •incin RaSeq) & (N in Za)) •imp ((F1~[N] in Ra) & (G1~[N] in Ra) & ((F1 •Ras_PLUS G1 in RaSeq) & ((F1 •Ras_PLUS G1)~[N] = (F1~[N]) •Ra_PLUS (G1~[N]))) & (((Ras_ABS(G1) in RaSeq) & (Ras_ABS(G1)~[N] = Ra_ABS(G1~[N])))) & (((Ras_Rev(G1) in RaSeq) & (Ras_Rev(G1)~[N] = Ra_Rev(G1~[N])))) & (((F1 •Ras_TIMES G1 in RaSeq) & (F1 •Ras_TIMES G1)~[N] = ((F1~[N]) •Ra_TIMES (G1~[N])))))
(698) Theorem 547: ((F in RaSeq) & (M = arb({h in Za | (FORALL i in (Za - h) | (F~[i]) /= Ra_0)}))) •imp (Ras_Recip(F) = Ras_Recip(shifted_seq(F,M)))
(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)
(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)
(710) Theorem 559: ({F,G} •incin RaSeq) •imp (F •Ras_PLUS G = G •Ras_PLUS F)
(711) Theorem 560: ({F,G} •incin RaSeq) •imp (F •Ras_TIMES G = G •Ras_TIMES F)
(712) Theorem 561: ({F,G,H} •incin RaSeq) •imp ((F •Ras_PLUS G) •Ras_PLUS H = F •Ras_PLUS (G •Ras_PLUS H))
(713) Theorem 562: ({F,G,H} •incin RaSeq) •imp ((F •Ras_TIMES G) •Ras_TIMES H = F •Ras_TIMES (G •Ras_TIMES H))
(714) Theorem 563: [Double-inversion law for rational sequences] (X in RaSeq) •imp (Ras_Rev(Ras_Rev(X))=X)
(715) Theorem 564: [Distributive law for multiplication of rational sequences] ({X,Y,V} •incin RaSeq) •imp ((X •Ras_TIMES (Y •Ras_PLUS V)) = ((X •Ras_TIMES Y) •Ras_PLUS (X •Ras_TIMES V)))
(716) Theorem 565: [Law of signs for multiplication of rational sequences] ({X,Y} •incin RaSeq) •imp ((X •Ras_TIMES Ras_Rev(Y)) = Ras_Rev(X •Ras_TIMES Y))
(717) Theorem 566: [Law of signs for multiplication of rational sequences, 2] ({X,Y} •incin RaSeq) •imp (((Ras_Rev(X) •Ras_TIMES Y) = Ras_Rev(X •Ras_TIMES Y)) & ((Ras_Rev(X) •Ras_TIMES Ras_Rev(Y)) = (X •Ras_TIMES Y)))
(718) Theorem 567: [Any rational sequence times 0 is 0] (X in RaSeq) •imp ((X •Ras_TIMES Ra0Seq) = Ra0Seq)
(719) Theorem 568: [0 is a right additive identity for rational sequences] (X in RaSeq) •imp (X •Ras_PLUS Ra0Seq = X)
(720) Theorem 569: [1 is a left multiplicative identity for rational sequences] (X in RaSeq) •imp (X •Ras_TIMES Ra1Seq = X)
(721) Theorem 570: [0 is right subtractive identity for rational sequence subtraction] (X in RaSeq) •imp (X •Ras_MINUS Ra0Seq = X)
(722) Theorem 571: [Basic properties of the signed negative for rational sequences] (X in RaSeq) •imp ((Ras_Rev(X) in RaSeq) & ((Ras_Rev(X) •Ras_PLUS X) = Ra0Seq) & (Ras_Rev(Ras_Rev(X)) = X))
(724) Theorem 573: [The negative of a sum of rational sequences is the sum of the negatives] ((X in RaSeq) & (Y in RaSeq)) •imp (Ras_Rev(X •Ras_PLUS Y) = Ras_Rev(X) •Ras_PLUS Ras_Rev(Y))
(725) Theorem 574: [A rational sequence minus itself gives 0] (X in RaSeq) •imp ((X •Ras_MINUS X) = Ra0Seq)
(726) Theorem 575: [Multiplication by Ras_Rev(Ra1Seq)] (X in RaSeq) •imp (Ras_Rev(X) = (Ras_Rev(Ra1Seq) •Ras_TIMES X))
(734) Theorem 583: [A rational sequence F and its additive inverse have the same absolute value] (F in RaSeq) •imp (Ras_ABS(Ras_Rev(F)) = Ras_ABS(F))
(735) Theorem 584: (F in RaSeq) •imp (((F •Ras_PLUS Ra0Seq) = F) & ((F •Ras_TIMES Ra1Seq) = F))
(741) Theorem 590: (X in Re) •imp ((arb(X) in RaCauchy) & (arb(X) in RaSeq) & (Cauchy_to_Re(arb(X)) = 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))
(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)))