---

Step * 1 1 of Lemma reals-uncountable

.....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))))))
BY
{ (InstConcl [⌜λn.(fst(primrec(n;<x, y>;f)))⌝;⌜λn.(snd(primrec(n;<x, y>;f)))⌝]⋅
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN SplitAndConcl
   THEN Try (Complete (Auto))) }

1
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))} )
⊢ ∀n:ℕ
    (((fst(primrec(n;<x, y>;f))) ≤ (fst(primrec(n + 1;<x, y>;f))))
    ∧ ((fst(primrec(n + 1;<x, y>;f))) < (snd(primrec(n + 1;<x, y>;f))))
    ∧ ((snd(primrec(n + 1;<x, y>;f))) ≤ (snd(primrec(n;<x, y>;f))))
    ∧ (((z n) < (fst(primrec(n + 1;<x, y>;f)))) ∨ ((snd(primrec(n + 1;<x, y>;f))) < (z n)))
    ∧ (((snd(primrec(n + 1;<x, y>;f))) - fst(primrec(n + 1;<x, y>;f))) < (r1/r(n + 1))))

---

Latex:

---

Latex:
.....assertion..... 
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{}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))))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}\mlambda{}n.(fst(primrec(n;<x,  y>f)))\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(snd(primrec(n;<x,  y>f)))\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  SplitAndConcl
  THEN  Try  (Complete  (Auto)))

---

Home Index