---

Step * 1 1 1 1 1 1 1 1 of Lemma continuous-limit


1. I : Interval
2. z : ℝ
3. x : ℕ ⟶ ℝ
4. z ∈ I
5. ∀n:ℕ. (x[n] ∈ I)
6. n : ℕ+
7. z ∈ i-approx(I;n)
8. N : ℕ
9. ∀n@0:ℕ. ((N ≤ n@0) ⇒ (|x[n@0] - z| ≤ (r1/r(2 * n))))
10. m : ℕ
11. N ≤ m
12. v : ℝ
13. x[m] = v ∈ ℝ
14. ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n))
15. (r1/r(2 * n)) ≤ r1
⊢ (v ∈ I) ⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n))))) ⇒ (v ∈ i-approx(I;2 * n))
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN Lemmaize [-7]) }

1
∀I:Interval. ∀z:ℝ. ∀n:ℕ+. ∀v:ℝ.
  ((z ∈ i-approx(I;n))
  ⇒ (((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n)))
  ⇒ ((r1/r(2 * n)) ≤ r1)
  ⇒ (v ∈ I)
  ⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n)))))
  ⇒ (v ∈ i-approx(I;2 * n)))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  z  :  \mBbbR{}
3.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
4.  z  \mmember{}  I
5.  \mforall{}n:\mBbbN{}.  (x[n]  \mmember{}  I)
6.  n  :  \mBbbN{}\msupplus{}
7.  z  \mmember{}  i-approx(I;n)
8.  N  :  \mBbbN{}
9.  \mforall{}n@0:\mBbbN{}.  ((N  \mleq{}  n@0)  {}\mRightarrow{}  (|x[n@0]  -  z|  \mleq{}  (r1/r(2  *  n))))
10.  m  :  \mBbbN{}
11.  N  \mleq{}  m
12.  v  :  \mBbbR{}
13.  x[m]  =  v
14.  ((r1/r(2  *  n))  +  (r1/r(2  *  n)))  =  (r1/r(n))
15.  (r1/r(2  *  n))  \mleq{}  r1
\mvdash{}  (v  \mmember{}  I)  {}\mRightarrow{}  (((z  -  (r1/r(2  *  n)))  \mleq{}  v)  \mwedge{}  (v  \mleq{}  (z  +  (r1/r(2  *  n)))))  {}\mRightarrow{}  (v  \mmember{}  i-approx(I;2  *  n))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  Lemmaize  [-7])

---

Home Index