---

Step * 1 of Lemma sinh-inv-sinh


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
BY
{ ((GenConclTerm ⌜ln(x + rsqrt((x * x) + r1))⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜expr(v)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜expr(-(v))⌝⋅ THENA Auto)) }

1
1. x : ℝ
2. (r0 ≤ ((x * x) + r1)) ∧ (r0 < (x + rsqrt((x * x) + r1)))
3. v : {x1:ℝ| x1 = rlog(x + rsqrt((x * x) + r1))} 
4. ln(x + rsqrt((x * x) + r1)) = v ∈ {x1:ℝ| x1 = rlog(x + rsqrt((x * x) + r1))} 
5. v1 : {y:ℝ| y = e^v} 
6. expr(v) = v1 ∈ {y:ℝ| y = e^v} 
7. v2 : {y:ℝ| y = e^-(v)} 
8. expr(-(v)) = v2 ∈ {y:ℝ| y = e^-(v)} 
⊢ (v1 - v2)/2 = x

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  (r0  \mleq{}  ((x  *  x)  +  r1))  \mwedge{}  (r0  <  (x  +  rsqrt((x  *  x)  +  r1)))
\mvdash{}  (expr(ln(x  +  rsqrt((x  *  x)  +  r1)))  -  expr(-(ln(x  +  rsqrt((x  *  x)  +  r1)))))/2  =  x


By

---

Latex:
((GenConclTerm  \mkleeneopen{}ln(x  +  rsqrt((x  *  x)  +  r1))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}expr(v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}expr(-(v))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index