---

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

∀a,b:ℝ. ∀f:[a, b] ⟶ℝ. ∀c:ℝ.
  ((∀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(f;a;b;c))
BY
{ TACTIC: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})))))
⊢ locally-non-constant(f;a;b;c)

2
1. a : ℝ
2. b : ℝ
3. f : [a, b] ⟶ℝ
4. c : ℝ
5. u : {u:ℝ| u ∈ [a, b]} 
6. v : {v:ℝ| v ∈ [a, b]} 
7. x : u < v
8. k : ℕ
9. F : ℕk + 1 ⟶ [a, b] ⟶ℝ
10. x1 : finite-deriv-seq([a, b];k;i,x.F[i;x])
11. x2 : ∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = (f(x) - c))
12. z : {z:ℝ| z ∈ [u, v]} 
13. i : ℕk + 1
⊢ z ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}c:\mBbbR{}.
    ((\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{}  locally-non-constant(f;a;b;c))


By

---

Latex:
TACTIC:Auto

---

Home Index