List of theorems referencing the symbol RAS_ABS
(676) Theorem 525: (X in Ra) •imp (Ras_ABS(Za •PROD {X}) = (Za •PROD {Ra_ABS(X)}))
(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))
(708) Theorem 557: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G)) •imp Ra_eqseq(Ras_ABS(F),Ras_ABS(G))
(728) Theorem 577: [The zero/unit sequence is its own absolute value] (Ras_ABS(Ra0Seq) = Ra0Seq) & (Ras_ABS(Ra1Seq) = Ra1Seq)
(729) Theorem 578: [?] ((H in RaCauchy) & Ra_eqseq(H,Ra0Seq)) •imp (Ra_eqseq(Ras_ABS(H),Ra0Seq) & (Ra_eqseq(Ras_Rev(H),Ra0Seq)))
(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)))
(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))
(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))))))
(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)))