List of theorems referencing the symbol DOT_RAS_PLUS
(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])))))
(688) Theorem 537: ({F,G} •incin RaCauchy) •imp (((F •Ras_PLUS G) in RaCauchy) & (Ras_ABS(F) in RaCauchy) & (Ras_Rev(F) 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)
(710) Theorem 559: ({F,G} •incin RaSeq) •imp (F •Ras_PLUS G = G •Ras_PLUS F)
(712) Theorem 561: ({F,G,H} •incin RaSeq) •imp ((F •Ras_PLUS G) •Ras_PLUS H = F •Ras_PLUS (G •Ras_PLUS H))
(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)))
(719) Theorem 568: [0 is a right additive identity for rational sequences] (X in RaSeq) •imp (X •Ras_PLUS 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))
(735) Theorem 584: (F in RaSeq) •imp (((F •Ras_PLUS Ra0Seq) = F) & ((F •Ras_TIMES Ra1Seq) = F))
(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)))
(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))))
(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)))
(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))))