---

Step * of Lemma rexp-rless

∀x,y:ℝ.  (x < y ⇐⇒ e^x < e^y)
BY
{ (Auto
   THEN Try ((FLemma `rexp_functionality_wrt_rless` [-1] THEN Complete (Auto)))
   THEN FLemma `rlog_functionality_wrt_rless` [-1]
   THEN Auto
   THEN RWO  "rlog-rexp" (-1)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Try  ((FLemma  `rexp\_functionality\_wrt\_rless`  [-1]  THEN  Complete  (Auto)))
  THEN  FLemma  `rlog\_functionality\_wrt\_rless`  [-1]
  THEN  Auto
  THEN  RWO    "rlog-rexp"  (-1)
  THEN  Auto)

---

Home Index