---

Step * 1 2 1 1 1 2 of Lemma reals-uncountable

.....upcase..... 
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 : ℕ
11. k : ℤ
12. [%13] : 0 < k
13. ((X i) ≤ (X (i + (k - 1)))) ∧ ((X (i + (k - 1))) < (Y (i + (k - 1)))) ∧ ((Y (i + (k - 1))) ≤ (Y i))
⊢ ((X i) ≤ (X (i + k))) ∧ ((X (i + k)) < (Y (i + k))) ∧ ((Y (i + k)) ≤ (Y i))
BY
{ (((InstHyp [⌜i + (k - 1)⌝] (-5))⋅ THENA (Auto THEN Auto')) THEN Subst' ((i + (k - 1)) + 1) = (i + k) ∈ ℤ -1 THEN Auto)
⋅ }

---

Latex:

---

Latex:
.....upcase..... 
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.  i  :  \mBbbN{}
11.  k  :  \mBbbZ{}
12.  [\%13]  :  0  <  k
13.  ((X  i)  \mleq{}  (X  (i  +  (k  -  1))))
\mwedge{}  ((X  (i  +  (k  -  1)))  <  (Y  (i  +  (k  -  1))))
\mwedge{}  ((Y  (i  +  (k  -  1)))  \mleq{}  (Y  i))
\mvdash{}  ((X  i)  \mleq{}  (X  (i  +  k)))  \mwedge{}  ((X  (i  +  k))  <  (Y  (i  +  k)))  \mwedge{}  ((Y  (i  +  k))  \mleq{}  (Y  i))


By

---

Latex:
(((InstHyp  [\mkleeneopen{}i  +  (k  -  1)\mkleeneclose{}]  (-5))\mcdot{}  THENA  (Auto  THEN  Auto'))
  THEN  Subst'  ((i  +  (k  -  1))  +  1)  =  (i  +  k)  -1
  THEN  Auto)\mcdot{}

---

Home Index