---

Step * 1 2 1 2 of Lemma reals-uncountable


1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. X : ℕ ⟶ ℝ
6. Y : ℕ ⟶ ℝ
7. (X 0) = x ∈ ℝ
8. (Y 0) = y ∈ ℝ
9. ∀n:ℕ
     (((X n) ≤ (X (n + 1)))
     ∧ ((X (n + 1)) < (Y (n + 1)))
     ∧ ((Y (n + 1)) ≤ (Y n))
     ∧ (((z n) < (X (n + 1))) ∨ ((Y (n + 1)) < (z n)))
     ∧ (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))))
10. ∀i,j:ℕ.  ((i ≤ j) ⇒ (((X i) ≤ (X j)) ∧ ((X j) < (Y j)) ∧ ((Y j) ≤ (Y i))))
⊢ ∃u:ℝ. ((x ≤ u) ∧ (u ≤ y) ∧ (∀n:ℕ. u ≠ z n))
BY
{ ((Assert ∀n:ℕ. (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))) BY
          Auto)⋅
   THEN (InstLemma `common-limit-squeeze` [⌜X⌝;⌜Y⌝;⌜λ2n.Y[n] - X[n]⌝]⋅ THENA Auto)
   ) }

1
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. X : ℕ ⟶ ℝ
6. Y : ℕ ⟶ ℝ
7. (X 0) = x ∈ ℝ
8. (Y 0) = y ∈ ℝ
9. ∀n:ℕ
     (((X n) ≤ (X (n + 1)))
     ∧ ((X (n + 1)) < (Y (n + 1)))
     ∧ ((Y (n + 1)) ≤ (Y n))
     ∧ (((z n) < (X (n + 1))) ∨ ((Y (n + 1)) < (z n)))
     ∧ (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))))
10. ∀i,j:ℕ.  ((i ≤ j) ⇒ (((X i) ≤ (X j)) ∧ ((X j) < (Y j)) ∧ ((Y j) ≤ (Y i))))
11. ∀n:ℕ. (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1)))
12. n : ℕ
13. X[n] ≤ X[n + 1]
⊢ X[n + 1] ≤ Y[n + 1]

2
.....antecedent..... 
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. X : ℕ ⟶ ℝ
6. Y : ℕ ⟶ ℝ
7. (X 0) = x ∈ ℝ
8. (Y 0) = y ∈ ℝ
9. ∀n:ℕ
     (((X n) ≤ (X (n + 1)))
     ∧ ((X (n + 1)) < (Y (n + 1)))
     ∧ ((Y (n + 1)) ≤ (Y n))
     ∧ (((z n) < (X (n + 1))) ∨ ((Y (n + 1)) < (z n)))
     ∧ (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))))
10. ∀i,j:ℕ.  ((i ≤ j) ⇒ (((X i) ≤ (X j)) ∧ ((X j) < (Y j)) ∧ ((Y j) ≤ (Y i))))
11. ∀n:ℕ. (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1)))
⊢ lim n→∞.Y[n] - X[n] = r0

3
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. X : ℕ ⟶ ℝ
6. Y : ℕ ⟶ ℝ
7. (X 0) = x ∈ ℝ
8. (Y 0) = y ∈ ℝ
9. ∀n:ℕ
     (((X n) ≤ (X (n + 1)))
     ∧ ((X (n + 1)) < (Y (n + 1)))
     ∧ ((Y (n + 1)) ≤ (Y n))
     ∧ (((z n) < (X (n + 1))) ∨ ((Y (n + 1)) < (z n)))
     ∧ (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))))
10. ∀i,j:ℕ.  ((i ≤ j) ⇒ (((X i) ≤ (X j)) ∧ ((X j) < (Y j)) ∧ ((Y j) ≤ (Y i))))
11. ∀n:ℕ. (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1)))
12. n : ℕ
⊢ r0≤Y[n] - X[n]≤Y[n] - X[n]

4
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. X : ℕ ⟶ ℝ
6. Y : ℕ ⟶ ℝ
7. (X 0) = x ∈ ℝ
8. (Y 0) = y ∈ ℝ
9. ∀n:ℕ
     (((X n) ≤ (X (n + 1)))
     ∧ ((X (n + 1)) < (Y (n + 1)))
     ∧ ((Y (n + 1)) ≤ (Y n))
     ∧ (((z n) < (X (n + 1))) ∨ ((Y (n + 1)) < (z n)))
     ∧ (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1))))
10. ∀i,j:ℕ.  ((i ≤ j) ⇒ (((X i) ≤ (X j)) ∧ ((X j) < (Y j)) ∧ ((Y j) ≤ (Y i))))
11. ∀n:ℕ. (((Y (n + 1)) - X (n + 1)) < (r1/r(n + 1)))
12. ∃y:ℝ. (lim n→∞.X[n] = y ∧ lim n→∞.Y[n] = y)
⊢ ∃u:ℝ. ((x ≤ u) ∧ (u ≤ y) ∧ (∀n:ℕ. u ≠ z n))

---

Latex:

---

Latex:

1.  z  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbR{}
3.  y  :  \mBbbR{}
4.  x  <  y
5.  X  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
6.  Y  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
7.  (X  0)  =  x
8.  (Y  0)  =  y
9.  \mforall{}n:\mBbbN{}
          (((X  n)  \mleq{}  (X  (n  +  1)))
          \mwedge{}  ((X  (n  +  1))  <  (Y  (n  +  1)))
          \mwedge{}  ((Y  (n  +  1))  \mleq{}  (Y  n))
          \mwedge{}  (((z  n)  <  (X  (n  +  1)))  \mvee{}  ((Y  (n  +  1))  <  (z  n)))
          \mwedge{}  (((Y  (n  +  1))  -  X  (n  +  1))  <  (r1/r(n  +  1))))
10.  \mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (((X  i)  \mleq{}  (X  j))  \mwedge{}  ((X  j)  <  (Y  j))  \mwedge{}  ((Y  j)  \mleq{}  (Y  i))))
\mvdash{}  \mexists{}u:\mBbbR{}.  ((x  \mleq{}  u)  \mwedge{}  (u  \mleq{}  y)  \mwedge{}  (\mforall{}n:\mBbbN{}.  u  \mneq{}  z  n))


By

---

Latex:
((Assert  \mforall{}n:\mBbbN{}.  (((Y  (n  +  1))  -  X  (n  +  1))  <  (r1/r(n  +  1)))  BY
                Auto)\mcdot{}
  THEN  (InstLemma  `common-limit-squeeze`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.Y[n]  -  X[n]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index