---

Step * of Lemma rational-IVT

∀a,b:ℝ. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [a, b]}  ⟶ ℝ]
    ∃c:{c:ℝ| c ∈ (a, b)}  [(g[c] = r0)] 
    supposing (a < b)
    ∧ ((g[a] * g[b]) < r0)
    ∧ (∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (g[x] = g[y])))
    ∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [a, b]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
BY
{ Auto }

1
1. a : ℝ
2. b : ℝ
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. [g] : {x:ℝ| x ∈ [a, b]}  ⟶ ℝ
5. [%] : (a < b)
∧ ((g[a] * g[b]) < r0)
∧ (∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [a, b]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
⊢ ∃c:{c:ℝ| c ∈ (a, b)}  [(g[c] = r0)]

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}f:(\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}).
    \mforall{}[g:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    {}\mrightarrow{}  \mBbbR{}]
        \mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  (a,  b)\}    [(g[c]  =  r0)] 
        supposing  (a  <  b)
        \mwedge{}  ((g[a]  *  g[b])  <  r0)
        \mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
        \mwedge{}  (\mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((ratreal(r)  \mmember{}  [a,  b])  {}\mRightarrow{}  (g[ratreal(r)]  =  ratreal(f[r]))))


By

---

Latex:
Auto

---

Home Index