---

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


1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. c : ℕ ⟶ ℝ
4. ∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n]))
5. ∀k:ℕ+. ∀large(n).{|c[n] - r0| ≤ (r1/r(k))}
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
7. y : ℝ
8. ∀k:ℕ+. ∀large(n).{|a[n] - y| ≤ (r1/r(k))}
9. k : ℕ+
10. ∀large(n).{|c[n] - r0| ≤ (r1/r(2 * k))}
11. ∀large(n).{|a[n] - y| ≤ (r1/r(2 * k))}
12. N : ℕ
13. ∀n:ℕ. ((N ≤ n) ⇒ ((|a[n] - y| ≤ (r1/r(2 * k))) ∧ (|c[n] - r0| ≤ (r1/r(2 * k)))))
14. n : ℕ
15. N ≤ n
16. |a[n] - y| ≤ (r1/r(2 * k))
17. |c[n] - r0| ≤ (r1/r(2 * k))
⊢ |b[n] - y| ≤ (r1/r(k))
BY
{ (Assert |b[n] - a[n]| ≤ c[n] BY
         OnMaybeHyp 6 (\h. (((InstHyp [⌜n⌝] h)⋅ THENA Auto) THEN D -1 THEN RWO "rabs-of-nonneg" 0 THEN Auto))) }

1
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. c : ℕ ⟶ ℝ
4. ∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n]))
5. ∀k:ℕ+. ∀large(n).{|c[n] - r0| ≤ (r1/r(k))}
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
7. y : ℝ
8. ∀k:ℕ+. ∀large(n).{|a[n] - y| ≤ (r1/r(k))}
9. k : ℕ+
10. ∀large(n).{|c[n] - r0| ≤ (r1/r(2 * k))}
11. ∀large(n).{|a[n] - y| ≤ (r1/r(2 * k))}
12. N : ℕ
13. ∀n:ℕ. ((N ≤ n) ⇒ ((|a[n] - y| ≤ (r1/r(2 * k))) ∧ (|c[n] - r0| ≤ (r1/r(2 * k)))))
14. n : ℕ
15. N ≤ n
16. |a[n] - y| ≤ (r1/r(2 * k))
17. |c[n] - r0| ≤ (r1/r(2 * k))
18. |b[n] - a[n]| ≤ c[n]
⊢ |b[n] - y| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  c  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}n:\mBbbN{}.  ((a[n]  \mleq{}  a[n  +  1])  \mwedge{}  (a[n  +  1]  \mleq{}  b[n  +  1])  \mwedge{}  (b[n  +  1]  \mleq{}  b[n]))
5.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}large(n).\{|c[n]  -  r0|  \mleq{}  (r1/r(k))\}
6.  \mforall{}n:\mBbbN{}.  r0\mleq{}b[n]  -  a[n]\mleq{}c[n]
7.  y  :  \mBbbR{}
8.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}large(n).\{|a[n]  -  y|  \mleq{}  (r1/r(k))\}
9.  k  :  \mBbbN{}\msupplus{}
10.  \mforall{}large(n).\{|c[n]  -  r0|  \mleq{}  (r1/r(2  *  k))\}
11.  \mforall{}large(n).\{|a[n]  -  y|  \mleq{}  (r1/r(2  *  k))\}
12.  N  :  \mBbbN{}
13.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  ((|a[n]  -  y|  \mleq{}  (r1/r(2  *  k)))  \mwedge{}  (|c[n]  -  r0|  \mleq{}  (r1/r(2  *  k)))))
14.  n  :  \mBbbN{}
15.  N  \mleq{}  n
16.  |a[n]  -  y|  \mleq{}  (r1/r(2  *  k))
17.  |c[n]  -  r0|  \mleq{}  (r1/r(2  *  k))
\mvdash{}  |b[n]  -  y|  \mleq{}  (r1/r(k))


By

---

Latex:
(Assert  |b[n]  -  a[n]|  \mleq{}  c[n]  BY
              OnMaybeHyp  6  (\mbackslash{}h.  (((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)
                                                    THEN  D  -1
                                                    THEN  RWO  "rabs-of-nonneg"  0
                                                    THEN  Auto)))

---

Home Index