---

Step * 1 1 of Lemma rlog-rexp

.....assertion..... 
1. x : ℝ
⊢ d(rlog(e^x))/dx = λx.(r1/e^x) * e^x on (-∞, ∞)
BY
{ (InstLemma `chain-rule` [⌜(-∞, ∞)⌝;⌜(r0, ∞)⌝;⌜λ2x.e^x⌝;⌜λ2x.e^x⌝;⌜λ2x.rlog(x)⌝;⌜λ2x.(r1/x)⌝]⋅
   THEN Auto
   THEN Try ((RWO "-1" 0 THEN Auto))) }

1
.....antecedent..... 
1. x : ℝ
⊢ maps-compact((-∞, ∞);(r0, ∞);x.e^x)

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
\mvdash{}  d(rlog(e\^{}x))/dx  =  \mlambda{}x.(r1/e\^{}x)  *  e\^{}x  on  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `chain-rule`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}(r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rlog(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/x)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))

---

Home Index