---

Step * of Lemma inv-sinh-sinh

∀[x:ℝ]. (inv-sinh(sinh(x)) = x)
BY
{ (Auto
   THEN (InstLemma `inv-sinh-domain` [⌜sinh(x)⌝]⋅ THENA Auto)
   THEN RepUR ``inv-sinh`` 0
   THEN (BLemma `ln-req-iff` THENA Auto)) }

1
1. x : ℝ
2. (r0 ≤ ((sinh(x) * sinh(x)) + r1)) ∧ (r0 < (sinh(x) + rsqrt((sinh(x) * sinh(x)) + r1)))
⊢ (sinh(x) + rsqrt((sinh(x) * sinh(x)) + r1)) = expr(x)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `inv-sinh-domain`  [\mkleeneopen{}sinh(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``inv-sinh``  0
  THEN  (BLemma  `ln-req-iff`  THENA  Auto))

---

Home Index