---

Step * 1 of Lemma rcos-seq-converges


∃c:{2...}
 ∃m:ℕ+
  ((∀n:ℕ+. ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1/r(c)) * (rcos-seq(n) - rcos-seq(n - 1)))))
  ∧ ((r(c) * (rcos-seq(1) - rcos-seq(0))/r(c - 1)) ≤ (r1/r(m))))
BY
{ (InstConcl [⌜3164556962025316455⌝;⌜1000000000⌝]⋅ THEN Auto) }

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

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

---

Latex:

---

Latex:

\mexists{}c:\{2...\}
  \mexists{}m:\mBbbN{}\msupplus{}
    ((\mforall{}n:\mBbbN{}\msupplus{}.  ((rcos-seq(n  +  1)  -  rcos-seq(n))  \mleq{}  ((r1/r(c))  *  (rcos-seq(n)  -  rcos-seq(n  -  1)))))
    \mwedge{}  ((r(c)  *  (rcos-seq(1)  -  rcos-seq(0))/r(c  -  1))  \mleq{}  (r1/r(m))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}3164556962025316455\mkleeneclose{};\mkleeneopen{}1000000000\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index