---

Step * of Lemma rexp-rleq

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

---

Latex:

---

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


By

---

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

---

Home Index