List of theorems referencing the symbol RAS_RECIP

(698) Theorem 547: ((F in RaSeq) & (M = arb({h in Za | (FORALL i in (Za - h) | (F~[i]) /= Ra_0)}))) •imp (Ras_Recip(F) = Ras_Recip(shifted_seq(F,M)))
(700) Theorem 549: ((F in RaCauchy) & (not Ra_eqseq(F,Ra0Seq))) •imp (EXISTS g in RaCauchy | Ra_eqseq(F,g) & (Ras_Recip(F) = Ras_Recip(g)) & (FORALL i in Za | ((g~[i]) /= Ra_0) & (Ras_Recip(g)~[i] = Recip(g~[i]))))
(701) Theorem 550: [The reciprocal of a non-null rational sequence is a rational sequence] ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (Ras_Recip(G) in RaSeq)
(702) Theorem 551: [Reciprocal and quotient of rational Cauchy sequences are, when defined, Cauchy sequences] (({F,G} •incin RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp ((Ras_Recip(G) in RaCauchy) & ((F •Ras_OVER G) in RaCauchy))
(709) Theorem 558: (({F,G} •incin RaCauchy) & Ra_eqseq(F,G) & (not(Ra_eqseq(F,Ra0Seq)))) •imp Ra_eqseq(Ras_Recip(F),Ras_Recip(G))
(723) Theorem 572: [Reciprocal sequence principle] ((X in RaCauchy) & (not Ra_eqseq(X,Ra0Seq))) •imp Ra_eqseq(X •Ras_TIMES Ras_Recip(X),Ra1Seq)