---

Step * 2 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. lim n→∞.c[n] = r0
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
7. ∃y:ℝ. lim n→∞.a[n] = y
⊢ ∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)
BY
{ ((ParallelLast THEN Auto) THEN All (Unfold `converges-to`) 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:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|c[n] - r0| ≤ (r1/r(k)))))])
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
7. y : ℝ
8. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(k)))))])
9. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|a[n] - y| ≤ (r1/r(k)))))])
10. k : ℕ+
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ 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.  lim  n\mrightarrow{}\minfty{}.c[n]  =  r0
6.  \mforall{}n:\mBbbN{}.  r0\mleq{}b[n]  -  a[n]\mleq{}c[n]
7.  \mexists{}y:\mBbbR{}.  lim  n\mrightarrow{}\minfty{}.a[n]  =  y
\mvdash{}  \mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.a[n]  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.b[n]  =  y)


By

---

Latex:
((ParallelLast  THEN  Auto)  THEN  All  (Unfold  `converges-to`)  THEN  Auto)

---

Home Index