---

Step * of Lemma rexp_wf

∀[x:ℝ]. (e^x ∈ ℝ)
BY
{ (Auto THEN Unfold `rexp` 0 THEN GenConclAtAddr [2;1;1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (e\^{}x  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto  THEN  Unfold  `rexp`  0  THEN  GenConclAtAddr  [2;1;1]  THEN  Auto)

---

Home Index