---

Step * of Lemma sinh-inv-sinh

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

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

---

Latex:

---

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


By

---

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

---

Home Index