Proof of Nuprl Lemma : derivative-implies-strictly-decreasing-closed

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

.....assertion.....
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-increasing for x ∈ [a, b]
BY
{ (InstLemma `derivative-implies-strictly-increasing-closed`
        [⌜a⌝;⌜b⌝;⌜λ₂x.-(f[x])⌝;⌜λ₂x.-(f'[x])⌝]⋅
   THEN Auto
   THEN (Assert (a, b) ⊆ [a, b]  BY
               (D 0 THEN Reduce 0 THEN Auto))
   THEN Try ((nRAdd ⌜f'[x]⌝ 0⋅ THEN 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)
9. (a, b) ⊆ [a, b]
⊢ d(-(f[x]))/dx = λx.-(f'[x]) on [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)} . (f'[x] < r0)
9. (a, b) ⊆ [a, b]
⊢ ifun(λx.-(f'[x]);[a, b])

Latex:

Latex:
.....assertion..... 1. a : \mBbbR{} 2. b : \{b:\mBbbR{}| a < b\} 3. f : [a, b] {}\mrightarrow{}\mBbbR{} 4. f' : [a, b] {}\mrightarrow{}\mBbbR{} 5. d(f[x])/dx = \mlambda{}x.f'[x] on [a, b] 6. ifun(\mlambda{}x.f'[x];[a, b]) 7. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (f'[x] \mleq{} r0) 8. \mforall{}x:\{x:\mBbbR{}| x \mmember{} (a, b)\} . (f'[x] < r0) \mvdash{} -(f[x]) strictly-increasing for x \mmember{} [a, b] By Latex: (InstLemma `derivative-implies-strictly-increasing-closed` [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(f[x])\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(f'[x])\mkleeneclose{}]\mcdot{} THEN Auto THEN (Assert (a, b) \msubseteq{} [a, b] BY (D 0 THEN Reduce 0 THEN Auto)) THEN Try ((nRAdd \mkleeneopen{}f'[x]\mkleeneclose{} 0\mcdot{} THEN Auto))) Home Index