---

Step * 1 1 of Lemma rcos-seq-increasing


1. ∀n:ℕ. ((r0 < rcos-seq(n)) ∧ (∀t:{t:ℝ| t ∈ [r0, rcos-seq(n)]} . (r0 < rcos(t))))
2. n : ℕ
3. (r0 < rcos-seq(n)) ∧ (∀t:{t:ℝ| t ∈ [r0, rcos-seq(n)]} . (r0 < rcos(t)))
⊢ rcos-seq(n) < (rcos-seq(n) + rcos(rcos-seq(n)))
BY
{ (nRAdd ⌜-(rcos-seq(n))⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}n:\mBbbN{}.  ((r0  <  rcos-seq(n))  \mwedge{}  (\mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  rcos-seq(n)]\}  .  (r0  <  rcos(t))))
2.  n  :  \mBbbN{}
3.  (r0  <  rcos-seq(n))  \mwedge{}  (\mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  rcos-seq(n)]\}  .  (r0  <  rcos(t)))
\mvdash{}  rcos-seq(n)  <  (rcos-seq(n)  +  rcos(rcos-seq(n)))


By

---

Latex:
(nRAdd  \mkleeneopen{}-(rcos-seq(n))\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index