---

Step * 1 1 of Lemma locally-non-constant-deriv-seq-test

.....assertion..... 
1. a : ℝ
2. b : ℝ
3. f : [a, b] ⟶ℝ
4. c : ℝ
5. ∀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})))))
⊢ locally-non-constant(λx.(f(x) - c);a;b;r0)
BY
{ TACTIC:(BLemma `locally-non-zero-finite-deriv-seq` THEN Try (Complete (Auto))) }

1
1. a : ℝ
2. b : ℝ
3. f : [a, b] ⟶ℝ
4. c : ℝ
5. ∀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})))))
⊢ ∀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] = λx.(f(x) - c)(x)))
          ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k})))))

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  c  :  \mBbbR{}
5.  \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\})))))
\mvdash{}  locally-non-constant(\mlambda{}x.(f(x)  -  c);a;b;r0)


By

---

Latex:
TACTIC:(BLemma  `locally-non-zero-finite-deriv-seq`  THEN  Try  (Complete  (Auto)))

---

Home Index