---

Step * of Lemma rcos-seq-differences

∀n:ℕ. (0 < n ⇒ ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1 - rsin(rcos-seq(n - 1))) * (rcos-seq(n) - rcos-seq(n - 1)))))
BY
{ (Auto
   THEN BLemma `rleq-iff-all-rless`
   THEN Auto
   THEN (Subst' rcos-seq(n + 1) - rcos-seq(n) ~ rcos-seq(n + 1) - rcos-seq((n - 1) + 1) 0 THENA Auto)
   THEN (RWO "rcos-seq-step" 0 THENA Auto)) }

1
1. n : ℕ
2. 0 < n
3. e : {e:ℝ| r0 < e} 
⊢ ((rcos-seq(n) + rcos(rcos-seq(n))) - rcos-seq(n - 1) + rcos(rcos-seq(n - 1))) ≤ (((r1 - rsin(rcos-seq(n - 1)))
* (rcos-seq(n) - rcos-seq(n - 1)))
+ e)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    (0  <  n
    {}\mRightarrow{}  ((rcos-seq(n  +  1)  -  rcos-seq(n))  \mleq{}  ((r1  -  rsin(rcos-seq(n  -  1)))
          *  (rcos-seq(n)  -  rcos-seq(n  -  1)))))


By

---

Latex:
(Auto
  THEN  BLemma  `rleq-iff-all-rless`
  THEN  Auto
  THEN  (Subst'  rcos-seq(n  +  1)  -  rcos-seq(n)  \msim{}  rcos-seq(n  +  1)  -  rcos-seq((n  -  1)  +  1)  0  THENA  Auto)
  THEN  (RWO  "rcos-seq-step"  0  THENA  Auto))

---

Home Index