---

Step * of Lemma derivative-is-zero

∀I:Interval. (iproper(I) ⇒ (∀f:I ⟶ℝ. (d(f[x])/dx = λx.r0 on I ⇐⇒ ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (f[x] = c))))
BY
{ Auto }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. d(f[x])/dx = λx.r0 on I
⊢ ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (f[x] = c)

2
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. ∃c:ℝ. ∀x:{x:ℝ| x ∈ I} . (f[x] = c)
⊢ d(f[x])/dx = λx.r0 on I

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)  {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  (d(f[x])/dx  =  \mlambda{}x.r0  on  I  \mLeftarrow{}{}\mRightarrow{}  \mexists{}c:\mBbbR{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[x]  =  c))))


By

---

Latex:
Auto

---

Home Index