---

Step * 1 1 1 of Lemma rcos-seq-converges


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)))
BY
{ ((InstLemma `rcos-seq-increasing` [⌜n - 1⌝]⋅ THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n -1 THENA Auto)
   THEN (Assert r0 < (rcos-seq(n) - rcos-seq(n - 1)) BY
               (nRAdd ⌜rcos-seq(n - 1)⌝ 0⋅ THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜rcos-seq(n) - rcos-seq(n - 1)⌝⋅ 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)))
3. rcos-seq(n - 1) < rcos-seq(n)
4. v : ℝ
5. (rcos-seq(n) - rcos-seq(n - 1)) = v ∈ ℝ
⊢ (r0 < v) ⇒ (((r1 - rsin(rcos-seq(n - 1))) * v) ≤ ((r1/r(3164556962025316455)) * v))

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `rcos-seq-increasing`  [\mkleeneopen{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -1  THENA  Auto)
  THEN  (Assert  r0  <  (rcos-seq(n)  -  rcos-seq(n  -  1))  BY
                          (nRAdd  \mkleeneopen{}rcos-seq(n  -  1)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}rcos-seq(n)  -  rcos-seq(n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index