---

Step * of Lemma cosh-rminus

∀[x:ℝ]. (cosh(-(x)) = cosh(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{}].  (cosh(-(x))  =  cosh(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