---

Step * 2 of Lemma derivative-cosh


1. d(e^-(x))/dx = λx.r(-1) * e^-(x) on (-∞, ∞)
⊢ d((expr(x) + expr(-(x)))/2)/dx = λx.(expr(x) - expr(-(x)))/2 on (-∞, ∞)
BY
{ ((Assert d((r1/r(2)) * (e^x + e^-(x)))/dx = λx.(r1/r(2)) * (e^x + (r(-1) * e^-(x))) on (-∞, ∞) BY
          (ProveDerivative THEN Auto))
   THEN DerivativeFunctionality (-1)
   THEN Auto
   THEN (RWW "int-rdiv-req expr-req" 0 THEN Auto)
   THEN nRMul ⌜r(2)⌝ 0⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  d(e\^{}-(x))/dx  =  \mlambda{}x.r(-1)  *  e\^{}-(x)  on  (-\minfty{},  \minfty{})
\mvdash{}  d((expr(x)  +  expr(-(x)))/2)/dx  =  \mlambda{}x.(expr(x)  -  expr(-(x)))/2  on  (-\minfty{},  \minfty{})


By

---

Latex:
((Assert  d((r1/r(2))  *  (e\^{}x  +  e\^{}-(x)))/dx  =  \mlambda{}x.(r1/r(2))  *  (e\^{}x  +  (r(-1)  *  e\^{}-(x)))  on  (-\minfty{},  \minfty{})  BY
                (ProveDerivative  THEN  Auto))
  THEN  DerivativeFunctionality  (-1)
  THEN  Auto
  THEN  (RWW  "int-rdiv-req  expr-req"  0  THEN  Auto)
  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index