List of theorems referencing the symbol RA1SEQ

(677) Theorem 526: {Ra0Seq,Ra1Seq} •incin RaCauchy
(680) Theorem 529: (U in Za) •imp (((Ra0Seq~[U]) = Ra_0) & ((Ra1Seq~[U]) = Ra_1))
(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))
(728) Theorem 577: [The zero/unit sequence is its own absolute value] (Ras_ABS(Ra0Seq) = Ra0Seq) & (Ras_ABS(Ra1Seq) = Ra1Seq)
(733) Theorem 582: [The unit Cauchy sequences Ra0Seq,Ra1Seq differ from one another] (not Ra_eqseq(Ra0Seq,Ra1Seq))
(735) Theorem 584: (F in RaSeq) •imp (((F •Ras_PLUS Ra0Seq) = F) & ((F •Ras_TIMES Ra1Seq) = F))