---

Step * 1 1 1 2 1 of Lemma common-limit-midpoints


1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. n : ℕ
7. r(-n) ≤ |a[0] - b[0]|
8. |a[0] - b[0]| ≤ r(n)
9. y : ℝ
10. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(k)))))])
11. k : ℕ+
12. ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(2 * k)))))]
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|b[n] - y| ≤ (r1/r(k)))))]
BY
{ Assert ⌜∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - b[n]| ≤ (r1/r(2 * k)))))]⌝⋅ }

1
.....assertion..... 
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. n : ℕ
7. r(-n) ≤ |a[0] - b[0]|
8. |a[0] - b[0]| ≤ r(n)
9. y : ℝ
10. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(k)))))])
11. k : ℕ+
12. ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(2 * k)))))]
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - b[n]| ≤ (r1/r(2 * k)))))]

2
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. n : ℕ
7. r(-n) ≤ |a[0] - b[0]|
8. |a[0] - b[0]| ≤ r(n)
9. y : ℝ
10. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(k)))))])
11. k : ℕ+
12. ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(2 * k)))))]
13. ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - b[n]| ≤ (r1/r(2 * k)))))]
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|b[n] - y| ≤ (r1/r(k)))))]

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}n:\mBbbN{}
          (((a[n  +  1]  =  a[n])  \mwedge{}  (b[n  +  1]  =  (a[n]  +  b[n]/r(2))))
          \mvee{}  ((a[n  +  1]  =  (a[n]  +  b[n]/r(2)))  \mwedge{}  (b[n  +  1]  =  b[n])))
4.  \mforall{}n:\mBbbN{}.  ((r(2\^{}n)  *  |a[n]  -  b[n]|)  \mleq{}  |a[0]  -  b[0]|)
5.  \mforall{}n,d:\mBbbN{}.
          (((r(2\^{}n)  *  |a[n]  -  a[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |a[n]  -  b[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |b[n]  -  a[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |b[n]  -  b[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|))
6.  n  :  \mBbbN{}
7.  r(-n)  \mleq{}  |a[0]  -  b[0]|
8.  |a[0]  -  b[0]|  \mleq{}  r(n)
9.  y  :  \mBbbR{}
10.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|a[n]  -  y|  \mleq{}  (r1/r(k)))))])
11.  k  :  \mBbbN{}\msupplus{}
12.  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|a[n]  -  y|  \mleq{}  (r1/r(2  *  k)))))]
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|b[n]  -  y|  \mleq{}  (r1/r(k)))))]


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|a[n]  -  b[n]|  \mleq{}  (r1/r(2  *  k)))))]\mkleeneclose{}\mcdot{}

---

Home Index