List of theorems referencing the symbol RAS_REV
(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))
(707) Theorem 556: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_Rev(F),Ras_Rev(G))
(714) Theorem 563: [Double-inversion law for rational sequences] (X in RaSeq) •imp (Ras_Rev(Ras_Rev(X))=X)
(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)))
(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))
(726) Theorem 575: [Multiplication by Ras_Rev(Ra1Seq)] (X in RaSeq) •imp (Ras_Rev(X) = (Ras_Rev(Ra1Seq) •Ras_TIMES X))
(727) Theorem 576: [The zero sequence is its own negative] Ras_Rev(Ra0Seq) = Ra0Seq
(729) Theorem 578: [?] ((H in RaCauchy) & Ra_eqseq(H,Ra0Seq)) •imp (Ra_eqseq(Ras_ABS(H),Ra0Seq) & (Ra_eqseq(Ras_Rev(H),Ra0Seq)))
(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)))
(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))
(752) Theorem 601: [Lemma for law of signs] (X in RaCauchy) •imp (Cauchy_to_Re(Ras_Rev(X)) = R_Rev(Cauchy_to_Re(X)))