---

Step * of Lemma IVT-deriv-seq-test

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:[a, b] ⟶ℝ.
  ∀c:ℝ
    ((f(a) ≤ c)
    ⇒ (c ≤ f(b))
    ⇒ (∀u,v:{v:ℝ| v ∈ [a, b]} .
          ((u < v)
          ⇒ (∃k:ℕ
               ∃F:ℕk + 1 ⟶ [a, b] ⟶ℝ
                (finite-deriv-seq([a, b];k;i,x.F[i;x])
                ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = (f(x) - c)))
                ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k}))))))
    ⇒ (∃x:ℝ [((x ∈ [a, b]) ∧ (f(x) = c))])) 
  supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (Auto
   THEN Try (((All Reduce THEN Auto) THEN DSetVars THEN Unhide THEN Complete (Auto)))
   THEN BLemma `IVT-locally-non-constant`
   THEN Auto
   THEN Try ((BLemma `locally-non-constant-deriv-seq-test` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    \mforall{}c:\mBbbR{}
        ((f(a)  \mleq{}  c)
        {}\mRightarrow{}  (c  \mleq{}  f(b))
        {}\mRightarrow{}  (\mforall{}u,v:\{v:\mBbbR{}|  v  \mmember{}  [a,  b]\}  .
                    ((u  <  v)
                    {}\mRightarrow{}  (\mexists{}k:\mBbbN{}
                              \mexists{}F:\mBbbN{}k  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
                                (finite-deriv-seq([a,  b];k;i,x.F[i;x])
                                \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (F[0;x]  =  (f(x)  -  c)))
                                \mwedge{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [u,  v]\}  .  (r0  <  \mSigma{}\{|F[i;z]|  |  0\mleq{}i\mleq{}k\}))))))
        {}\mRightarrow{}  (\mexists{}x:\mBbbR{}  [((x  \mmember{}  [a,  b])  \mwedge{}  (f(x)  =  c))])) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


By

---

Latex:
(Auto
  THEN  Try  (((All  Reduce  THEN  Auto)  THEN  DSetVars  THEN  Unhide  THEN  Complete  (Auto)))
  THEN  BLemma  `IVT-locally-non-constant`
  THEN  Auto
  THEN  Try  ((BLemma  `locally-non-constant-deriv-seq-test`  THEN  Auto)))

---

Home Index