---

Step * 1 1 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. 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}
14. u ≤ z
15. z ≤ v
16. u ≤ z
17. z ≤ v
⊢ f(z) ≠ r0
BY
{ TACTIC:(RWO "rsum_single" (-5) THENA Auto) }

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[0;z]|
14. u ≤ z
15. z ≤ v
16. u ≤ z
17. z ≤ v
⊢ f(z) ≠ r0

---

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.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
9.  F  :  \mBbbN{}0  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
10.  finite-deriv-seq([a,  b];0;i,x.F[i;x])
11.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (F[0;x]  =  f(x))
12.  z  :  \{z:\mBbbR{}|  z  \mmember{}  [u,  v]\} 
13.  r0  <  \mSigma{}\{|F[i;z]|  |  0\mleq{}i\mleq{}0\}
14.  u  \mleq{}  z
15.  z  \mleq{}  v
16.  u  \mleq{}  z
17.  z  \mleq{}  v
\mvdash{}  f(z)  \mneq{}  r0


By

---

Latex:
TACTIC:(RWO  "rsum\_single"  (-5)  THENA  Auto)

---

Home Index