---

Step * of Lemma derivative-implies-strictly-decreasing

∀I:Interval
  (iproper(I)
  ⇒ (∀f,f':I ⟶ℝ.
        (d(f[x])/dx = λx.f'[x] on I
        ⇒ f'[x] continuous for x ∈ I
        ⇒ (∀x:{x:ℝ| x ∈ I} . (f'[x] < r0))
        ⇒ f[x] strictly-decreasing for x ∈ I)))
BY
{ (Auto THEN Assert ⌜-(f[x]) strictly-increasing for x ∈ I⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on I
6. f'[x] continuous for x ∈ I
7. ∀x:{x:ℝ| x ∈ I} . (f'[x] < r0)
⊢ -(f[x]) strictly-increasing for x ∈ I

2
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on I
6. f'[x] continuous for x ∈ I
7. ∀x:{x:ℝ| x ∈ I} . (f'[x] < r0)
8. -(f[x]) strictly-increasing for x ∈ I
⊢ f[x] strictly-decreasing for x ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.
                (d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
                {}\mRightarrow{}  f'[x]  continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f'[x]  <  r0))
                {}\mRightarrow{}  f[x]  strictly-decreasing  for  x  \mmember{}  I)))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}-(f[x])  strictly-increasing  for  x  \mmember{}  I\mkleeneclose{}\mcdot{})

---

Home Index