---

Step * 2 3 of Lemma rational-IVT-1


1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. [g] : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. [%] : (ratreal(a) ≤ ratreal(b))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. s : ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
7. ∀i:ℕ
     ((ratreal(fst((s i))) ∈ [ratreal(a), ratreal(b)])
     ∧ (ratreal(snd((s i))) ∈ [ratreal(a), ratreal(b)])
     ∧ (ratreal(fst((s i))) ≤ ratreal(fst((s (i + 1)))))
     ∧ (ratreal(fst((s i))) ≤ ratreal(snd((s i))))
     ∧ (ratreal(snd((s (i + 1)))) ≤ ratreal(snd((s i))))
     ∧ (g[ratreal(fst((s i)))] ≤ r0)
     ∧ (r0 ≤ g[ratreal(snd((s i)))])
     ∧ ((ratreal(snd((s i))) - ratreal(fst((s i)))) = (rinv(r(2))^i * (ratreal(b) - ratreal(a)))))
8. ∃y:ℝ. (lim n→∞.ratreal(fst((s n))) = y ∧ lim n→∞.ratreal(snd((s n))) = y)
⊢ ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = r0)]
BY
{ (ExRepD
   THEN (Assert y ∈ [ratreal(a), ratreal(b)] BY
               (Reduce 0
                THEN (InstLemma `rleq-limit-constant` [⌜ratreal(b)⌝;⌜λ2n.ratreal(fst((s n)))⌝;⌜y⌝]⋅ THENA Auto)
                THEN InstLemma `constant-rleq-limit` [⌜ratreal(a)⌝;⌜λ2n.ratreal(fst((s n)))⌝;⌜y⌝]⋅
                THEN Auto))
   THEN (D 0 With ⌜y⌝  THENA Auto)) }

1
1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. (ratreal(a) ≤ ratreal(b))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
6. s : ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
7. ∀i:ℕ
     ((ratreal(fst((s i))) ∈ [ratreal(a), ratreal(b)])
     ∧ (ratreal(snd((s i))) ∈ [ratreal(a), ratreal(b)])
     ∧ (ratreal(fst((s i))) ≤ ratreal(fst((s (i + 1)))))
     ∧ (ratreal(fst((s i))) ≤ ratreal(snd((s i))))
     ∧ (ratreal(snd((s (i + 1)))) ≤ ratreal(snd((s i))))
     ∧ (g[ratreal(fst((s i)))] ≤ r0)
     ∧ (r0 ≤ g[ratreal(snd((s i)))])
     ∧ ((ratreal(snd((s i))) - ratreal(fst((s i)))) = (rinv(r(2))^i * (ratreal(b) - ratreal(a)))))
8. y : ℝ
9. lim n→∞.ratreal(fst((s n))) = y
10. lim n→∞.ratreal(snd((s n))) = y
11. y ∈ [ratreal(a), ratreal(b)]
⊢ g[y] = r0

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  b  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
3.  f  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
4.  [g]  :  \{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}    {}\mrightarrow{}  \mBbbR{}
5.  [\%]  :  (ratreal(a)  \mleq{}  ratreal(b))
\mwedge{}  (ratreal(f[a])  \mleq{}  r0)
\mwedge{}  (r0  \mleq{}  ratreal(f[b]))
\mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
\mwedge{}  (\mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((ratreal(r)  \mmember{}  [ratreal(a),  ratreal(b)])  {}\mRightarrow{}  (g[ratreal(r)]  =  ratreal(f[r]))))
6.  s  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
7.  \mforall{}i:\mBbbN{}
          ((ratreal(fst((s  i)))  \mmember{}  [ratreal(a),  ratreal(b)])
          \mwedge{}  (ratreal(snd((s  i)))  \mmember{}  [ratreal(a),  ratreal(b)])
          \mwedge{}  (ratreal(fst((s  i)))  \mleq{}  ratreal(fst((s  (i  +  1)))))
          \mwedge{}  (ratreal(fst((s  i)))  \mleq{}  ratreal(snd((s  i))))
          \mwedge{}  (ratreal(snd((s  (i  +  1))))  \mleq{}  ratreal(snd((s  i))))
          \mwedge{}  (g[ratreal(fst((s  i)))]  \mleq{}  r0)
          \mwedge{}  (r0  \mleq{}  g[ratreal(snd((s  i)))])
          \mwedge{}  ((ratreal(snd((s  i)))  -  ratreal(fst((s  i))))  =  (rinv(r(2))\^{}i  *  (ratreal(b)  -  ratreal(a)))))
8.  \mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.ratreal(fst((s  n)))  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.ratreal(snd((s  n)))  =  y)
\mvdash{}  \mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  [ratreal(a),  ratreal(b)]\}    [(g[c]  =  r0)]


By

---

Latex:
(ExRepD
  THEN  (Assert  y  \mmember{}  [ratreal(a),  ratreal(b)]  BY
                          (Reduce  0
                            THEN  (InstLemma  `rleq-limit-constant`  [\mkleeneopen{}ratreal(b)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.ratreal(fst((s  n)))\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
                                        THENA  Auto
                                        )
                            THEN  InstLemma  `constant-rleq-limit`  [\mkleeneopen{}ratreal(a)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.ratreal(fst((s  n)))\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}y\mkleeneclose{}    THENA  Auto))

---

Home Index