---

Step * of Lemma rcos-seq-positive

∀n:ℕ. ((r0 < rcos-seq(n)) ∧ (∀t:{t:ℝ| t ∈ [r0, rcos-seq(n)]} . (r0 < rcos(t))))
BY
{ (InductionOnNat THEN Reduce 0) }

1
(r0 < rcos-seq(0)) ∧ (∀t:{t:ℝ| (r0 ≤ t) ∧ (t ≤ rcos-seq(0))} . (r0 < rcos(t)))

2
1. n : ℤ
2. [%1] : 0 < n
3. (r0 < rcos-seq(n - 1)) ∧ (∀t:{t:ℝ| t ∈ [r0, rcos-seq(n - 1)]} . (r0 < rcos(t)))
⊢ (r0 < rcos-seq(n)) ∧ (∀t:{t:ℝ| (r0 ≤ t) ∧ (t ≤ rcos-seq(n))} . (r0 < rcos(t)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  ((r0  <  rcos-seq(n))  \mwedge{}  (\mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r0,  rcos-seq(n)]\}  .  (r0  <  rcos(t))))


By

---

Latex:
(InductionOnNat  THEN  Reduce  0)

---

Home Index