---

Step * 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])
⊢ ∃z:{z:ℝ| z ∈ [a, b]} . f(z) ≠ c
BY
{ ((Assert ∃del:{ℝ| ((r0 < del)
                    ∧ (∀y:ℝ
                         ((y ∈ [a, b])
                         ⇒ (|y - z| ≤ del)
                         ⇒ (|f(y) - f(z) - f'(z) * (y - z)| ≤ ((r1/r(2 * k)) * |y - z|)))))} BY
          ((With ⌜2 * k⌝ (D 6)⋅ THENA Auto)
           THEN (InstHyp [⌜1⌝] (-1)⋅ THENA (Auto THEN RepUR ``i-approx iproper i-finite`` 0 THEN EAuto 1))
           THEN ParallelLast
           THEN Auto
           THEN DVar `z'
           THEN Unhide
           THEN Auto))
   THEN D -1
   ) }

1
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. [%12] : (r0 < del)
∧ (∀y:ℝ. ((y ∈ [a, b]) ⇒ (|y - z| ≤ del) ⇒ (|f(y) - f(z) - f'(z) * (y - z)| ≤ ((r1/r(2 * k)) * |y - z|))))
⊢ ∃z:{z:ℝ| z ∈ [a, b]} . f(z) ≠ c

---

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])
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [a,  b]\}  .  f(z)  \mneq{}  c


By

---

Latex:
((Assert  \mexists{}del:\{\mBbbR{}|  ((r0  <  del)
                                    \mwedge{}  (\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|)))))\}  BY
                ((With  \mkleeneopen{}2  *  k\mkleeneclose{}  (D  6)\mcdot{}  THENA  Auto)
                  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}
                              THENA  (Auto  THEN  RepUR  ``i-approx  iproper  i-finite``  0  THEN  EAuto  1)
                              )
                  THEN  ParallelLast
                  THEN  Auto
                  THEN  DVar  `z'
                  THEN  Unhide
                  THEN  Auto))
  THEN  D  -1
  )

---

Home Index