---

Step * of Lemma sinh-rminus

∀[x:ℝ]. (sinh(-(x)) = -(sinh(x)))
BY
{ (Auto
   THEN RepUR ``cosh sinh`` 0
   THEN (RWO "int-rdiv-req" 0 THENA Auto)
   THEN (nRMul ⌜r(2)⌝ 0⋅ THENA Auto)
   THEN (RWO "expr-req" 0 THEN Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (sinh(-(x))  =  -(sinh(x)))


By

---

Latex:
(Auto
  THEN  RepUR  ``cosh  sinh``  0
  THEN  (RWO  "int-rdiv-req"  0  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "expr-req"  0  THEN  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index