---

Step * of Lemma rexp-rminus

∀[x:ℝ]. (e^-(x) = (r1/e^x))
BY
{ (Auto THEN nRMul ⌜e^x⌝ 0⋅) }

1
1. x : ℝ
⊢ (e^-(x) * e^x) = r1

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (e\^{}-(x)  =  (r1/e\^{}x))


By

---

Latex:
(Auto  THEN  nRMul  \mkleeneopen{}e\^{}x\mkleeneclose{}  0\mcdot{})

---

Home Index