---

Step * 1 1 1 1 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. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|c[n] - r0| ≤ (r1/r(k)))))])
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
7. k : ℕ+
8. N : ℕ
9. ∀n:ℕ. ((N ≤ n) ⇒ (|c[n] - r0| ≤ (r1/r(k))))
10. n : ℕ
11. m : ℕ
12. N ≤ n
13. N ≤ m
14. d : ℤ
15. 0 < d
16. ∀n,m:ℕ.  (((m - n) = (d - 1) ∈ ℤ) ⇒ a[n]≤a[m]≤b[n])
17. n1 : ℕ
18. m1 : ℕ
19. (m1 - n1) = d ∈ ℤ
⊢ a[n1]≤a[m1]≤b[n1]
BY
{ ((InstHyp [⌜n1 + 1⌝; ⌜m1⌝] (-4))⋅ THENA 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. k : ℕ+
8. N : ℕ
9. ∀n:ℕ. ((N ≤ n) ⇒ (|c[n] - r0| ≤ (r1/r(k))))
10. n : ℕ
11. m : ℕ
12. N ≤ n
13. N ≤ m
14. d : ℤ
15. 0 < d
16. ∀n,m:ℕ.  (((m - n) = (d - 1) ∈ ℤ) ⇒ a[n]≤a[m]≤b[n])
17. n1 : ℕ
18. m1 : ℕ
19. (m1 - n1) = d ∈ ℤ
20. a[n1 + 1]≤a[m1]≤b[n1 + 1]
⊢ a[n1]≤a[m1]≤b[n1]

---

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{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|c[n]  -  r0|  \mleq{}  (r1/r(k)))))])
6.  \mforall{}n:\mBbbN{}.  r0\mleq{}b[n]  -  a[n]\mleq{}c[n]
7.  k  :  \mBbbN{}\msupplus{}
8.  N  :  \mBbbN{}
9.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|c[n]  -  r0|  \mleq{}  (r1/r(k))))
10.  n  :  \mBbbN{}
11.  m  :  \mBbbN{}
12.  N  \mleq{}  n
13.  N  \mleq{}  m
14.  d  :  \mBbbZ{}
15.  0  <  d
16.  \mforall{}n,m:\mBbbN{}.    (((m  -  n)  =  (d  -  1))  {}\mRightarrow{}  a[n]\mleq{}a[m]\mleq{}b[n])
17.  n1  :  \mBbbN{}
18.  m1  :  \mBbbN{}
19.  (m1  -  n1)  =  d
\mvdash{}  a[n1]\mleq{}a[m1]\mleq{}b[n1]


By

---

Latex:
((InstHyp  [\mkleeneopen{}n1  +  1\mkleeneclose{};  \mkleeneopen{}m1\mkleeneclose{}]  (-4))\mcdot{}  THENA  Auto)

---

Home Index