---

Step * 1 of Lemma rational-fun-zero_wf


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]))))
⊢ rational-fun-zero(f;a;b) ∈ {c:ℝ| (c ∈ [ratreal(a), ratreal(b)]) ∧ (g[c] = r0)} 
BY
{ (Assert TERMOF{rational-IVT-2:o, \\v:l} 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
         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. TERMOF{rational-IVT-2:o, \\v:l} 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]))))
⊢ rational-fun-zero(f;a;b) ∈ {c:ℝ| (c ∈ [ratreal(a), ratreal(b)]) ∧ (g[c] = 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]))))
\mvdash{}  rational-fun-zero(f;a;b)  \mmember{}  \{c:\mBbbR{}|  (c  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (g[c]  =  r0)\} 


By

---

Latex:
(Assert  TERMOF\{rational-IVT-2:o,  \mbackslash{}\mbackslash{}v:l\}  a  b  \mmember{}  \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]  =  r\000C0)] 
                                                                                                    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
              Auto)

---

Home Index