List of theorems referencing the symbol DOT_RAS_TIMES
(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])))))
(693) Theorem 542: ({F,G} •incin RaCauchy) •imp (((F •Ras_MINUS G) in RaCauchy) & ((F •Ras_TIMES G) in RaCauchy))
(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)
(711) Theorem 560: ({F,G} •incin RaSeq) •imp (F •Ras_TIMES G = G •Ras_TIMES F)
(713) Theorem 562: ({F,G,H} •incin RaSeq) •imp ((F •Ras_TIMES G) •Ras_TIMES H = F •Ras_TIMES (G •Ras_TIMES 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)))
(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)
(720) Theorem 569: [1 is a left multiplicative identity for rational sequences] (X in RaSeq) •imp (X •Ras_TIMES Ra1Seq = X)
(723) Theorem 572: [Reciprocal sequence principle] ((X in RaCauchy) & (not Ra_eqseq(X,Ra0Seq))) •imp Ra_eqseq(X •Ras_TIMES Ras_Recip(X),Ra1Seq)
(726) Theorem 575: [Multiplication by Ras_Rev(Ra1Seq)] (X in RaSeq) •imp (Ras_Rev(X) = (Ras_Rev(Ra1Seq) •Ras_TIMES X))
(735) Theorem 584: (F in RaSeq) •imp (((F •Ras_PLUS Ra0Seq) = F) & ((F •Ras_TIMES Ra1Seq) = F))
(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)))
(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)))
(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))))