---

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


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[0;z]| + Σ{|F[i;z]| | 0 + 1≤i≤k})
17. u ≤ z
18. z ≤ v
19. r0 < Σ{|F[i;z]| | 0 + 1≤i≤k}
20. z1 : ℝ
21. u ≤ z1
22. z1 ≤ v
23. F[1;z1] ≠ r0
24. d(f[x])/dx = λx.F[1;x] on [a, b]
25. k1 : ℕ+
26. (r1/r(k1)) < |F[1;z1]|
27. ∀f':[u, v] ⟶ℝ
      (d(f x)/dx = λx.f' x on [u, v]
      ⇒ (∃z:{z:ℝ| (u ≤ z) ∧ (z ≤ v)} . f' z ≠ r0)
      ⇒ (∀c:ℝ. ∃z:{z:ℝ| (u ≤ z) ∧ (z ≤ v)} . f z ≠ c))
⊢ d(f x)/dx = λx.F[1;x] on [u, v]
BY
{ TACTIC:(InstLemma `derivative_functionality_wrt_subinterval` [⌜[a, b]⌝;⌜[u, v]⌝]⋅ THEN Auto THEN BHyp -1 THEN Auto) }

1
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[0;z]| + Σ{|F[i;z]| | 0 + 1≤i≤k})
17. u ≤ z
18. z ≤ v
19. r0 < Σ{|F[i;z]| | 0 + 1≤i≤k}
20. z1 : ℝ
21. u ≤ z1
22. z1 ≤ v
23. F[1;z1] ≠ r0
24. d(f[x])/dx = λx.F[1;x] on [a, b]
25. k1 : ℕ+
26. (r1/r(k1)) < |F[1;z1]|
27. ∀f':[u, v] ⟶ℝ
      (d(f x)/dx = λx.f' x on [u, v]
      ⇒ (∃z:{z:ℝ| (u ≤ z) ∧ (z ≤ v)} . f' z ≠ r0)
      ⇒ (∀c:ℝ. ∃z:{z:ℝ| (u ≤ z) ∧ (z ≤ v)} . f z ≠ c))
28. ∀[f,f':[a, b] ⟶ℝ].  ([u, v] ⊆ [a, b]  ⇒ d(f[x])/dx = λx.f'[x] on [a, b] ⇒ d(f[x])/dx = λx.f'[x] on [u, v])
⊢ [u, v] ⊆ [a, b] 

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  u  :  \mBbbR{}
4.  v  :  \mBbbR{}
5.  a  \mleq{}  u
6.  u  <  v
7.  v  \mleq{}  b
8.  k  :  \mBbbZ{}
9.  [\%4]  :  0  <  k
10.  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}
            ((\mexists{}F:\mBbbN{}(k  -  1)  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
                  (finite-deriv-seq([a,  b];k  -  1;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  -  1\}))))
            {}\mRightarrow{}  (\mexists{}z:\mBbbR{}.  ((u  \mleq{}  z)  \mwedge{}  (z  \mleq{}  v)  \mwedge{}  f(z)  \mneq{}  r0)))
11.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
12.  F  :  \mBbbN{}k  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
13.  finite-deriv-seq([a,  b];k;i,x.F[i;x])
14.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (F[0;x]  =  f(x))
15.  z  :  \{z:\mBbbR{}|  z  \mmember{}  [u,  v]\} 
16.  r0  <  (|F[0;z]|  +  \mSigma{}\{|F[i;z]|  |  0  +  1\mleq{}i\mleq{}k\})
17.  u  \mleq{}  z
18.  z  \mleq{}  v
19.  r0  <  \mSigma{}\{|F[i;z]|  |  0  +  1\mleq{}i\mleq{}k\}
20.  z1  :  \mBbbR{}
21.  u  \mleq{}  z1
22.  z1  \mleq{}  v
23.  F[1;z1]  \mneq{}  r0
24.  d(f[x])/dx  =  \mlambda{}x.F[1;x]  on  [a,  b]
25.  k1  :  \mBbbN{}\msupplus{}
26.  (r1/r(k1))  <  |F[1;z1]|
27.  \mforall{}f':[u,  v]  {}\mrightarrow{}\mBbbR{}
            (d(f  x)/dx  =  \mlambda{}x.f'  x  on  [u,  v]
            {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  (u  \mleq{}  z)  \mwedge{}  (z  \mleq{}  v)\}  .  f'  z  \mneq{}  r0)
            {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  \mexists{}z:\{z:\mBbbR{}|  (u  \mleq{}  z)  \mwedge{}  (z  \mleq{}  v)\}  .  f  z  \mneq{}  c))
\mvdash{}  d(f  x)/dx  =  \mlambda{}x.F[1;x]  on  [u,  v]


By

---

Latex:
TACTIC:(InstLemma  `derivative\_functionality\_wrt\_subinterval`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}[u,  v]\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  BHyp  -1
                THEN  Auto)

---

Home Index