---

Step * of Lemma rcos-seq-converges

rcos-seq(n)↓ as n→∞
BY
{ (InstLemma `increasing-sequence-converges` [⌜λn.rcos-seq(n)⌝]⋅ THEN All Reduce THEN Auto) }

1
∃c:{2...}
 ∃m:ℕ+
  ((∀n:ℕ+. ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1/r(c)) * (rcos-seq(n) - rcos-seq(n - 1)))))
  ∧ ((r(c) * (rcos-seq(1) - rcos-seq(0))/r(c - 1)) ≤ (r1/r(m))))

---

Latex:

---

Latex:
rcos-seq(n)\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
(InstLemma  `increasing-sequence-converges`  [\mkleeneopen{}\mlambda{}n.rcos-seq(n)\mkleeneclose{}]\mcdot{}  THEN  All  Reduce  THEN  Auto)

---

Home Index