---

Step * 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 + 1)
BY
{ (RWO "rcos-seq-step" 0 THENA Auto) }

1
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)))

---

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  +  1)


By

---

Latex:
(RWO  "rcos-seq-step"  0  THENA  Auto)

---

Home Index