---

Step * 1 1 of Lemma rcos-seq-converges


1. n : ℕ+
⊢ (rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1/r(3164556962025316455)) * (rcos-seq(n) - rcos-seq(n - 1)))
BY
{ ((InstLemma `rcos-seq-differences` [⌜n⌝]⋅ THEN Auto) THEN (RWO "-1" 0 THENA Auto)) }

1
1. n : ℕ+
2. (rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1 - rsin(rcos-seq(n - 1))) * (rcos-seq(n) - rcos-seq(n - 1)))
⊢ ((r1 - rsin(rcos-seq(n - 1))) * (rcos-seq(n) - rcos-seq(n - 1))) ≤ ((r1/r(3164556962025316455))
* (rcos-seq(n) - rcos-seq(n - 1)))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  (rcos-seq(n  +  1)  -  rcos-seq(n))  \mleq{}  ((r1/r(3164556962025316455))  *  (rcos-seq(n)  -  rcos-seq(n  -  1)))


By

---

Latex:
((InstLemma  `rcos-seq-differences`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index