---

Step * of Lemma cosh-radd

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

1
1. x : ℝ
2. y : ℝ
⊢ (expr(x + y) + expr(-(x + y))) = ((expr(-(x)) * expr(-(y))) + (expr(x) * expr(y)))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (cosh(x  +  y)  =  ((cosh(x)  *  cosh(y))  +  (sinh(x)  *  sinh(y))))


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))

---

Home Index