---

Step * of Lemma ln-req-iff

∀[x:{x:ℝ| r0 < x} ]. ∀[y:ℝ].  uiff(ln(x) = y;x = expr(y))
BY
{ (Auto THEN RWO "-1 -1<" 0 THEN Auto) }

1
1. x : {x:ℝ| r0 < x} 
2. y : ℝ
3. ln(x) = y
⊢ x = expr(ln(x))

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r0  <  x\}  ].  \mforall{}[y:\mBbbR{}].    uiff(ln(x)  =  y;x  =  expr(y))


By

---

Latex:
(Auto  THEN  RWO  "-1  -1<"  0  THEN  Auto)

---

Home Index