---

Step * 1 of Lemma inv-sinh-sinh


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)
BY
{ ((Assert r1 ≤ cosh(x) BY
          Auto)
   THEN (Assert cosh(x) = rsqrt((sinh(x) * sinh(x)) + r1) BY
               ((BLemma `rsqrt-unique`  THENA (Auto THEN MemTypeCD THEN Auto THEN RWO "-1<" 0 THEN Auto))
                THEN (RWO "rnexp2<" 0 THENA Auto)
                THEN InstLemma `cosh2-sinh2` [⌜x⌝]⋅
                THEN Auto))
   THEN RWO  "-1<" 0
   THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  r1  \mleq{}  cosh(x)  BY
                Auto)
  THEN  (Assert  cosh(x)  =  rsqrt((sinh(x)  *  sinh(x))  +  r1)  BY
                          ((BLemma  `rsqrt-unique` 
                              THENA  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  RWO  "-1<"  0  THEN  Auto)
                              )
                            THEN  (RWO  "rnexp2<"  0  THENA  Auto)
                            THEN  InstLemma  `cosh2-sinh2`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  RWO    "-1<"  0
  THEN  Auto)

---

Home Index