---

Step * 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 ∈ ℝ
⊢ (v ∈ I) ⇒ (((z - (r1/r(2 * n))) ≤ v) ∧ (v ≤ (z + (r1/r(2 * n))))) ⇒ (v ∈ i-approx(I;2 * n))
BY
{ (Assert ((r1/r(2 * n)) + (r1/r(2 * n))) = (r1/r(n)) BY
         (RWO "radd-int-fractions" 0 THEN Auto)) }

1
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))
⊢ (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
\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:
(Assert  ((r1/r(2  *  n))  +  (r1/r(2  *  n)))  =  (r1/r(n))  BY
              (RWO  "radd-int-fractions"  0  THEN  Auto))

---

Home Index