---

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

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f,f':[a, b] ⟶ℝ.
  (d(f[x])/dx = λx.f'[x] on [a, b]
  ⇒ ifun(λx.f'[x];[a, b])
  ⇒ (∀x:{x:ℝ| x ∈ [a, b]} . (f'[x] ≤ r0))
  ⇒ (∀x:{x:ℝ| x ∈ (a, b)} . (f'[x] < r0))
  ⇒ f[x] strictly-decreasing for x ∈ [a, b])
BY
{ Auto }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. f' : [a, b] ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on [a, b]
6. ifun(λx.f'[x];[a, b])
7. ∀x:{x:ℝ| x ∈ [a, b]} . (f'[x] ≤ r0)
8. ∀x:{x:ℝ| x ∈ (a, b)} . (f'[x] < r0)
⊢ f[x] strictly-decreasing for x ∈ [a, b]

2
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. f' : [a, b] ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on [a, b]
6. ifun(λx.f'[x];[a, b])
7. ∀x:{x:ℝ| x ∈ [a, b]} . (f'[x] ≤ r0)
8. x : {x:ℝ| x ∈ (a, b)} 
⊢ x ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 

3
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. f' : [a, b] ⟶ℝ
5. d(f[x])/dx = λx.f'[x] on [a, b]
⊢ a ≤ b

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f,f':[a,  b]  {}\mrightarrow{}\mBbbR{}.
    (d(f[x])/dx  =  \mlambda{}x.f'[x]  on  [a,  b]
    {}\mRightarrow{}  ifun(\mlambda{}x.f'[x];[a,  b])
    {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (f'[x]  \mleq{}  r0))
    {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  (a,  b)\}  .  (f'[x]  <  r0))
    {}\mRightarrow{}  f[x]  strictly-decreasing  for  x  \mmember{}  [a,  b])


By

---

Latex:
Auto

---

Home Index