---

Step * 1 1 4 of Lemma log-by-IVT


1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ locally-non-constant(λx.real_exp(x);r(-1);r(n);a)
BY
{ (InstLemma `derivative-implies-strictly-increasing-simple` [⌜r(-1)⌝;⌜r(n)⌝;⌜λ2x.e^x⌝;⌜λ2x.real_exp(x)⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ d(e^x)/dx = λx.real_exp(x) on [r(-1), r(n)]

2
.....antecedent..... 
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ ifun(λx.real_exp(x);[r(-1), r(n)])

3
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. x : {x:ℝ| x ∈ [r(-1), r(n)]} 
⊢ r0 < real_exp(x)

4
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. e^x strictly-increasing for x ∈ [r(-1), r(n)]
⊢ locally-non-constant(λx.real_exp(x);r(-1);r(n);a)

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  (r1/r(2))  <  a\}  @i
2.  r0  <  a
3.  n  :  \mBbbN{}
4.  r(-n)  \mleq{}  a
5.  a  \mleq{}  r(n)
\mvdash{}  locally-non-constant(\mlambda{}x.real\_exp(x);r(-1);r(n);a)


By

---

Latex:
(InstLemma  `derivative-implies-strictly-increasing-simple`  [\mkleeneopen{}r(-1)\mkleeneclose{};\mkleeneopen{}r(n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}x.real\_exp(x)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index