---

Step * 1 of Lemma reals-uncountable


1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
⊢ ∃u:ℝ. ((x ≤ u) ∧ (u ≤ y) ∧ (∀n:ℕ. u ≠ z n))
BY
{ Assert ⌜∃X,Y:ℕ ⟶ ℝ
           (((X 0) = x ∈ ℝ)
           ∧ ((Y 0) = y ∈ ℝ)
           ∧ (∀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))))))⌝⋅ }

1
.....assertion..... 
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
⊢ ∃X,Y:ℕ ⟶ ℝ
   (((X 0) = x ∈ ℝ)
   ∧ ((Y 0) = y ∈ ℝ)
   ∧ (∀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))))))

2
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
8. ∃X,Y:ℕ ⟶ ℝ
    (((X 0) = x ∈ ℝ)
    ∧ ((Y 0) = y ∈ ℝ)
    ∧ (∀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))))))
⊢ ∃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.  f  :  \mBbbN{}  {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}    {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\} 
6.  \mforall{}n:\mBbbN{}.  \mforall{}p:\{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  .
          let  x,y  =  p 
          in  let  x',y'  =  f  n  p 
                in  (x  \mleq{}  x')
                      \mwedge{}  (x'  <  y')
                      \mwedge{}  (y'  \mleq{}  y)
                      \mwedge{}  (((z  n)  <  x')  \mvee{}  (y'  <  (z  n)))
                      \mwedge{}  ((y'  -  x')  <  (r1/r(n  +  1)))
7.  \mforall{}n:\mBbbN{}.  (primrec(n;<x,  y>f)  \mmember{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  )
\mvdash{}  \mexists{}u:\mBbbR{}.  ((x  \mleq{}  u)  \mwedge{}  (u  \mleq{}  y)  \mwedge{}  (\mforall{}n:\mBbbN{}.  u  \mneq{}  z  n))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}X,Y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
                  (((X  0)  =  x)
                  \mwedge{}  ((Y  0)  =  y)
                  \mwedge{}  (\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))))))\mkleeneclose{}\mcdot{}

---

Home Index