---

Step * of Lemma rlog-rexp

∀[x:ℝ]. (rlog(e^x) = x)
BY
{ (Auto
   THEN (InstLemma `antiderivatives-equal` [⌜(-∞, ∞)⌝;⌜λ2x.r1⌝;⌜λ2x.x⌝;⌜λ2x.rlog(e^x)⌝]⋅
   THENM (InstHyp [⌜x⌝] (-1)⋅ THEN Auto)
   )
   THEN Auto) }

1
.....antecedent..... 
1. x : ℝ
⊢ d(rlog(e^x))/dx = λx.r1 on (-∞, ∞)

2
.....antecedent..... 
1. x : ℝ
⊢ ∃x:{x:ℝ| x ∈ (-∞, ∞)} . (x = rlog(e^x))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `antiderivatives-equal`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rlog(e\^{}x)\mkleeneclose{}]\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  Auto)

---

Home Index