---

Step * 1 1 1 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))} )
8. n : ℕ
⊢ ((fst(primrec(n;<x, y>;f))) ≤ (fst((f n primrec(n;<x, y>;f)))))
∧ ((fst((f n primrec(n;<x, y>;f)))) < (snd((f n primrec(n;<x, y>;f)))))
∧ ((snd((f n primrec(n;<x, y>;f)))) ≤ (snd(primrec(n;<x, y>;f))))
∧ (((z n) < (fst((f n primrec(n;<x, y>;f))))) ∨ ((snd((f n primrec(n;<x, y>;f)))) < (z n)))
∧ (((snd((f n primrec(n;<x, y>;f)))) - fst((f n primrec(n;<x, y>;f)))) < (r1/r(n + 1)))
BY
{ (((InstHyp [⌜n⌝] (-2))⋅ THENA Auto)
   THEN (GenConclAtAddr [1; 1; 1])
   THEN ((InstHyp [⌜n⌝; ⌜v⌝] (-6))⋅ THENA Auto)
   THEN RepeatFor 2 (DVar `v')
   THEN All Reduce
   THEN (MoveToConcl (-1))
   THEN (GenConclAtAddr [1; 1])
   THEN RepeatFor 2 (DVar `v')
   THEN All Reduce
   THEN Auto)⋅ }

---

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))\}  )
8.  n  :  \mBbbN{}
\mvdash{}  ((fst(primrec(n;<x,  y>f)))  \mleq{}  (fst((f  n  primrec(n;<x,  y>f)))))
\mwedge{}  ((fst((f  n  primrec(n;<x,  y>f))))  <  (snd((f  n  primrec(n;<x,  y>f)))))
\mwedge{}  ((snd((f  n  primrec(n;<x,  y>f))))  \mleq{}  (snd(primrec(n;<x,  y>f))))
\mwedge{}  (((z  n)  <  (fst((f  n  primrec(n;<x,  y>f)))))  \mvee{}  ((snd((f  n  primrec(n;<x,  y>f))))  <  (z  n)))
\mwedge{}  (((snd((f  n  primrec(n;<x,  y>f))))  -  fst((f  n  primrec(n;<x,  y>f))))  <  (r1/r(n  +  1)))


By

---

Latex:
(((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddr  [1;  1;  1])
  THEN  ((InstHyp  [\mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}v\mkleeneclose{}]  (-6))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `v')
  THEN  All  Reduce
  THEN  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;  1])
  THEN  RepeatFor  2  (DVar  `v')
  THEN  All  Reduce
  THEN  Auto)\mcdot{}

---

Home Index