---

Step * 1 1 1 1 1 1 1 1 1 of Lemma non-zero-deriv-non-constant


1. a : ℝ
2. b : ℝ
3. a < b
4. f : [a, b] ⟶ℝ
5. f' : [a, b] ⟶ℝ
6. d(f(x))/dx = λx.f'(x) on [a, b]
7. z : {z:ℝ| z ∈ [a, b]} 
8. f'(z) ≠ r0
9. c : ℝ
10. k : ℕ+
11. (r1/r(k)) < |f'(z)|
12. icompact([a, b])
13. del : ℝ
14. r0 < del
15. ∀y:ℝ. ((y ∈ [a, b]) ⇒ (|y - z| ≤ del) ⇒ (|f(y) - f(z) - f'(z) * (y - z)| ≤ ((r1/r(2 * k)) * |y - z|)))
16. y : ℝ
17. y ∈ [a, b]
18. |y - z| ≤ del
19. |f(y) - f(z) - f'(z) * (y - z)| ≤ ((r1/r(2 * k)) * |y - z|)
20. |f'(z) * (y - z)| ≤ (((r1/r(2 * k)) * |y - z|) + |f(y) - f(z) - r0|)
21. |y - z| = |z - y|
⊢ ((r1/r(2 * k)) * |y - z|) ≤ |f(y) - f(z)|
BY
{ (MoveToConcl 11
   THEN MoveToConcl (-2)
   THEN GenConclTerms Auto [⌜f'(z)⌝;⌜y - z⌝;⌜f(y) - f(z)⌝]⋅
   THEN All Thin
   THEN Auto) }

1
1. k : ℕ+
2. v : ℝ
3. v1 : ℝ
4. v2 : ℝ
5. |v * v1| ≤ (((r1/r(2 * k)) * |v1|) + |v2 - r0|)
6. (r1/r(k)) < |v|
⊢ ((r1/r(2 * k)) * |v1|) ≤ |v2|

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
5.  f'  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
6.  d(f(x))/dx  =  \mlambda{}x.f'(x)  on  [a,  b]
7.  z  :  \{z:\mBbbR{}|  z  \mmember{}  [a,  b]\} 
8.  f'(z)  \mneq{}  r0
9.  c  :  \mBbbR{}
10.  k  :  \mBbbN{}\msupplus{}
11.  (r1/r(k))  <  |f'(z)|
12.  icompact([a,  b])
13.  del  :  \mBbbR{}
14.  r0  <  del
15.  \mforall{}y:\mBbbR{}
            ((y  \mmember{}  [a,  b])
            {}\mRightarrow{}  (|y  -  z|  \mleq{}  del)
            {}\mRightarrow{}  (|f(y)  -  f(z)  -  f'(z)  *  (y  -  z)|  \mleq{}  ((r1/r(2  *  k))  *  |y  -  z|)))
16.  y  :  \mBbbR{}
17.  y  \mmember{}  [a,  b]
18.  |y  -  z|  \mleq{}  del
19.  |f(y)  -  f(z)  -  f'(z)  *  (y  -  z)|  \mleq{}  ((r1/r(2  *  k))  *  |y  -  z|)
20.  |f'(z)  *  (y  -  z)|  \mleq{}  (((r1/r(2  *  k))  *  |y  -  z|)  +  |f(y)  -  f(z)  -  r0|)
21.  |y  -  z|  =  |z  -  y|
\mvdash{}  ((r1/r(2  *  k))  *  |y  -  z|)  \mleq{}  |f(y)  -  f(z)|


By

---

Latex:
(MoveToConcl  11
  THEN  MoveToConcl  (-2)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}f'(z)\mkleeneclose{};\mkleeneopen{}y  -  z\mkleeneclose{};\mkleeneopen{}f(y)  -  f(z)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto)

---

Home Index