---

Step * of Lemma rational_fun_zero_wf

∀a,b:ℝ. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [a, b]}  ⟶ ℝ]
    rational_fun_zero(f;a;b) ∈ {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
{ ((Intros THEN Unhide)
   THEN (Assert TERMOF{rational-IVT-ext:o, \\v:l} ∈ ∀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)
   THEN (Subst' rational_fun_zero(f;a;b) ~ TERMOF{rational-IVT-ext:o, \\v:l} a b f 0 THENA Computation)
   THEN GenConclAtAddr [2;1]
   THEN (D -2 With ⌜f⌝  THENA Auto)
   THEN SubsumeC ⌜∀[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]))))⌝⋅
   THEN Try (Eq)
   THEN (D 0 THENA Auto)
   THEN (D -1 With ⌜g⌝  THENA Auto)
   THEN SubsumeC ⌜∃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]))))⌝⋅
   THEN Try (Eq)
   THEN (D 0 THENA Auto)
   THEN RenameVar `xx' 5
   THEN D -1 With ⌜xx⌝ 
   THEN Try (Trivial)
   THEN SubsumeC ⌜∃c:{c:ℝ| c ∈ (a, b)}  [(g[c] = r0)]⌝⋅
   THEN Auto) }

---

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{}]
        rational\_fun\_zero(f;a;b)  \mmember{}  \{c:\mBbbR{}|  (c  \mmember{}  (a,  b))  \mwedge{}  (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:
((Intros  THEN  Unhide)
  THEN  (Assert  TERMOF\{rational-IVT-ext:o,  \mbackslash{}\mbackslash{}v:l\}  \mmember{}  \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
                          Auto)
  THEN  (Subst'  rational\_fun\_zero(f;a;b)  \msim{}  TERMOF\{rational-IVT-ext:o,  \mbackslash{}\mbackslash{}v:l\}  a  b  f  0
              THENA  Computation
              )
  THEN  GenConclAtAddr  [2;1]
  THEN  (D  -2  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\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]))))\mkleeneclose{}\mcdot{}
  THEN  Try  (Eq)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}g\mkleeneclose{}    THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\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]))))\mkleeneclose{}\mcdot{}
  THEN  Try  (Eq)
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `xx'  5
  THEN  D  -1  With  \mkleeneopen{}xx\mkleeneclose{} 
  THEN  Try  (Trivial)
  THEN  SubsumeC  \mkleeneopen{}\mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  (a,  b)\}    [(g[c]  =  r0)]\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index