---

Step * of Lemma rcos-seq-increasing

∀n:ℕ. (rcos-seq(n) < rcos-seq(n + 1))
BY
{ (InstLemma `rcos-seq-positive` [] THEN ParallelLast) }

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

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (rcos-seq(n)  <  rcos-seq(n  +  1))


By

---

Latex:
(InstLemma  `rcos-seq-positive`  []  THEN  ParallelLast)

---

Home Index