---

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

∀a,b:ℝ.
  ((a < b)
  ⇒ (∀f,f':[a, b] ⟶ℝ.
        (d(f(x))/dx = λx.f'(x) on [a, b]
        ⇒ (∃z:{z:ℝ| z ∈ [a, b]} . f'(z) ≠ r0)
        ⇒ (∀c:ℝ. ∃z:{z:ℝ| z ∈ [a, b]} . f(z) ≠ c))))
BY
{ (Auto THEN ExRepD THEN ((FLemma `small-reciprocal-rneq-zero` [-2]⋅ THENM D -1) THENA Auto)) }

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)|
⊢ ∃z:{z:ℝ| z ∈ [a, b]} . f(z) ≠ c

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    ((a  <  b)
    {}\mRightarrow{}  (\mforall{}f,f':[a,  b]  {}\mrightarrow{}\mBbbR{}.
                (d(f(x))/dx  =  \mlambda{}x.f'(x)  on  [a,  b]
                {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [a,  b]\}  .  f'(z)  \mneq{}  r0)
                {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  \mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [a,  b]\}  .  f(z)  \mneq{}  c))))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  ((FLemma  `small-reciprocal-rneq-zero`  [-2]\mcdot{}  THENM  D  -1)  THENA  Auto))

---

Home Index