---

Step * of Lemma locally-non-zero-finite-deriv-seq

∀a,b:ℝ. ∀f:[a, 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)))
            ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k}))))))
  ⇒ locally-non-constant(f;a;b;r0))
BY
{ (Auto
   THEN Try ((DSetVars THEN ∀h:hyp. RepUR ``i-member`` h  THEN MemTypeCD THEN Auto))
   THEN D 0
   THEN Auto
   THEN (InstHyp [⌜u⌝;⌜v⌝] 4⋅ THENA Auto)
   THEN Thin 4
   THEN D -1
   THEN MoveToConcl (-1)
   THEN MoveToConcl 3
   THEN NatInd (-1)
   THEN Auto
   THEN Try ((DSetVars THEN ∀h:hyp. RepUR ``i-member`` h  THEN MemTypeCD THEN Auto))
   THEN ExRepD) }

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

2
1. a : ℝ
2. b : ℝ
3. u : ℝ
4. v : ℝ
5. a ≤ u
6. u < v
7. v ≤ b
8. k : ℤ
9. [%4] : 0 < k
10. ∀f:[a, b] ⟶ℝ
      ((∃F:ℕ(k - 1) + 1 ⟶ [a, b] ⟶ℝ
         (finite-deriv-seq([a, b];k - 1;i,x.F[i;x])
         ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = f(x)))
         ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k - 1}))))
      ⇒ (∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ r0)))
11. f : [a, b] ⟶ℝ
12. F : ℕk + 1 ⟶ [a, b] ⟶ℝ
13. finite-deriv-seq([a, b];k;i,x.F[i;x])
14. ∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = f(x))
15. z : {z:ℝ| z ∈ [u, v]} 
16. r0 < Σ{|F[i;z]| | 0≤i≤k}
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ r0)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Try  ((DSetVars  THEN  \mforall{}h:hyp.  RepUR  ``i-member``  h    THEN  MemTypeCD  THEN  Auto))
  THEN  D  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  Thin  4
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  3
  THEN  NatInd  (-1)
  THEN  Auto
  THEN  Try  ((DSetVars  THEN  \mforall{}h:hyp.  RepUR  ``i-member``  h    THEN  MemTypeCD  THEN  Auto))
  THEN  ExRepD)

---

Home Index