---

Step * of Lemma rexp-difference-bound

∀x,y:ℝ.  ((x < y) ⇒ ((e^y - e^x) ≤ (e^y * (y - x))))
BY
{ (Auto
   THEN (InstLemma `mean-value-for-bounded-derivative` 
         [⌜[x, y]⌝;⌜λ2x.e^x⌝;⌜λ2x.e^x⌝;⌜e^y⌝]⋅
         THENA (Auto THEN RepUR ``iproper`` 0 THEN Auto)
         )
   ) }

1
.....antecedent..... 
1. x : ℝ
2. y : ℝ
3. x < y
⊢ d(e^x)/dx = λx.e^x on [x, y]

2
1. x : ℝ
2. y : ℝ
3. x < y
4. x1 : {x@0:ℝ| x@0 ∈ [x, y]} 
⊢ |e^x1| ≤ e^y

3
1. x : ℝ
2. y : ℝ
3. x < y
4. ∀x@0,y@0:{x@0:ℝ| x@0 ∈ [x, y]} .  (|e^x@0 - e^y@0| ≤ (e^y * |x@0 - y@0|))
⊢ (e^y - e^x) ≤ (e^y * (y - x))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  ((e\^{}y  -  e\^{}x)  \mleq{}  (e\^{}y  *  (y  -  x))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `mean-value-for-bounded-derivative` 
              [\mkleeneopen{}[x,  y]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}e\^{}y\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper``  0  THEN  Auto)
              )
  )

---

Home Index