---

Step * of Lemma common-limit-squeeze

No Annotations
∀a,b,c:ℕ ⟶ ℝ.
  ((∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n])))
  ⇒ lim n→∞.c[n] = r0
  ⇒ (∀n:ℕ. r0≤b[n] - a[n]≤c[n])
  ⇒ (∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)))
BY
{ (Auto THEN Assert ⌜∃y:ℝ. lim n→∞.a[n] = y⌝⋅) }

1
.....assertion..... 
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]
⊢ ∃y:ℝ. lim n→∞.a[n] = y

2
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b,c:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}n:\mBbbN{}.  ((a[n]  \mleq{}  a[n  +  1])  \mwedge{}  (a[n  +  1]  \mleq{}  b[n  +  1])  \mwedge{}  (b[n  +  1]  \mleq{}  b[n])))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.c[n]  =  r0
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  r0\mleq{}b[n]  -  a[n]\mleq{}c[n])
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.a[n]  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.b[n]  =  y)))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}y:\mBbbR{}.  lim  n\mrightarrow{}\minfty{}.a[n]  =  y\mkleeneclose{}\mcdot{})

---

Home Index