---

Step * 1 1 of Lemma inv-sinh-sinh


1. x : ℝ
2. r0 ≤ ((sinh(x) * sinh(x)) + r1)
3. r0 < (sinh(x) + rsqrt((sinh(x) * sinh(x)) + r1))
4. r1 ≤ cosh(x)
5. cosh(x) = rsqrt((sinh(x) * sinh(x)) + r1)
⊢ (sinh(x) + cosh(x)) = expr(x)
BY
{ (RepUR ``sinh cosh`` 0 THEN (RWO "int-rdiv-req" 0 THENM nRMul ⌜r(2)⌝ 0⋅) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  \mleq{}  ((sinh(x)  *  sinh(x))  +  r1)
3.  r0  <  (sinh(x)  +  rsqrt((sinh(x)  *  sinh(x))  +  r1))
4.  r1  \mleq{}  cosh(x)
5.  cosh(x)  =  rsqrt((sinh(x)  *  sinh(x))  +  r1)
\mvdash{}  (sinh(x)  +  cosh(x))  =  expr(x)


By

---

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

---

Home Index