---

Step * 1 of Lemma derivative-implies-strictly-decreasing

.....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
BY
{ (InstLemma `derivative-implies-strictly-increasing` 
        [⌜I⌝;⌜λ2x.-(f[x])⌝;⌜λ2x.-(f'[x])⌝]⋅
   THEN Auto
   THEN Try ((ProveDerivative THEN Auto))
   THEN Try ((nRAdd ⌜f'[x]⌝ 0⋅ THEN Auto))
   THEN BLemma `continuous-minus`
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  f'  :  I  {}\mrightarrow{}\mBbbR{}
5.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
6.  f'[x]  continuous  for  x  \mmember{}  I
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f'[x]  <  r0)
\mvdash{}  -(f[x])  strictly-increasing  for  x  \mmember{}  I


By

---

Latex:
(InstLemma  `derivative-implies-strictly-increasing` 
            [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(f[x])\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(f'[x])\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((ProveDerivative  THEN  Auto))
  THEN  Try  ((nRAdd  \mkleeneopen{}f'[x]\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  BLemma  `continuous-minus`
  THEN  Auto)

---

Home Index