---

Step * of Lemma rational-IVT-1

∀a,b:ℤ × ℕ+. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ]
    ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = r0)] 
    supposing (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]))))
BY
{ (Intros
   THEN Assert ⌜∃s:ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
                 ∀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)))))⌝⋅
   ) }

1
.....assertion..... 
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]))))
⊢ ∃s:ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
   ∀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)))))

2
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:ℕ ⟶ (ℤ × ℕ+ × ℤ × ℕ+)
    ∀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)))))
⊢ ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = r0)]

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  \mforall{}f:(\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}).
    \mforall{}[g:\{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}    {}\mrightarrow{}  \mBbbR{}]
        \mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  [ratreal(a),  ratreal(b)]\}    [(g[c]  =  r0)] 
        supposing  (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]))))


By

---

Latex:
(Intros
  THEN  Assert  \mkleeneopen{}\mexists{}s:\mBbbN{}  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
                              \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)))))\mkleeneclose{}\mcdot{}
  )

---

Home Index