---

Step * 1 of Lemma rexp-rlog


1. x : ℝ
2. r0 < x
⊢ e^rlog(x) = x
BY
{ ((BLemma `req-iff-not-rneq` THENA Auto) THEN (D 0 THENA Auto)) }

1
1. x : ℝ
2. r0 < x
3. e^rlog(x) ≠ x
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  x
\mvdash{}  e\^{}rlog(x)  =  x


By

---

Latex:
((BLemma  `req-iff-not-rneq`  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index