---

Step * 1 of Lemma derivative-cosh

.....assertion..... 
d(e^-(x))/dx = λx.r(-1) * e^-(x) on (-∞, ∞)
BY
{ (InstLemma `derivative-rexp-fun2` [⌜λ2x.-(x)⌝;⌜λ2x.r(-1)⌝]⋅ THEN Auto) }

1
1. d(e^-(x))/dx = λx.e^-(x) * r(-1) on (-∞, ∞)
⊢ d(e^-(x))/dx = λx.r(-1) * e^-(x) on (-∞, ∞)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `derivative-rexp-fun2`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.-(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r(-1)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index