---

Step * of Lemma rexp_functionality_wrt_rless

∀x,y:ℝ.  ((x < y) ⇒ (e^x < e^y))
BY
{ (InstLemma `rexp-of-positive` []
   THEN Auto
   THEN (Assert y = (x + (y - x)) BY
               (nRNorm 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO  "rexp-radd" 0 THENA Auto)) }

1
1. ∀x:ℝ. ((r0 < x) ⇒ (r1 < e^x))
2. x : ℝ
3. y : ℝ
4. x < y
5. y = (x + (y - x))
⊢ e^x < (e^x * e^y - x)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rexp-of-positive`  []
  THEN  Auto
  THEN  (Assert  y  =  (x  +  (y  -  x))  BY
                          (nRNorm  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO    "rexp-radd"  0  THENA  Auto))

---

Home Index