---

Step * of Lemma cosh-inv-cosh

∀[x:{x:ℝ| r1 ≤ x} ]. (cosh(inv-cosh(x)) = x)
BY
{ (Auto
   THEN (D -1 THEN (Unhide THENA Auto))
   THEN (Assert r1 ≤ (x * x) BY
               (DupHyp (-1) THEN nRMul ⌜x⌝ (-1)⋅ THEN Auto THEN RWO "-1<" 0 THEN Auto))
   THEN (Assert r0 ≤ ((x * x) - r1) BY
               ((RWO "-1<" 0 THENM nRNorm 0) THEN Auto))
   THEN (Assert r0 ≤ rsqrt((x * x) - r1) BY
               (BLemma `rsqrt_nonneg` THEN Auto))
   THEN (Assert r1 ≤ (x + rsqrt((x * x) - r1)) BY
               ((RWO "-1<" 0 THENM nRNorm 0) THEN Auto))
   THEN (Assert r0 < (x + rsqrt((x * x) - r1)) BY
               (RWO  "-1<" 0 THEN Auto))
   THEN RepUR ``cosh inv-cosh`` 0
   THEN (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. r1 ≤ x
3. r1 ≤ (x * x)
4. r0 ≤ ((x * x) - r1)
5. r0 ≤ rsqrt((x * x) - r1)
6. r1 ≤ (x + rsqrt((x * x) - r1))
7. r0 < (x + rsqrt((x * x) - r1))
8. v : {x1:ℝ| x1 = rlog(x + rsqrt((x * x) - r1))} 
9. ln(x + rsqrt((x * x) - r1)) = v ∈ {x1:ℝ| x1 = rlog(x + rsqrt((x * x) - r1))} 
10. v1 : {y:ℝ| y = e^v} 
11. expr(v) = v1 ∈ {y:ℝ| y = e^v} 
12. v2 : {y:ℝ| y = e^-(v)} 
13. expr(-(v)) = v2 ∈ {y:ℝ| y = e^-(v)} 
⊢ (v1 + v2)/2 = x

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r1  \mleq{}  x\}  ].  (cosh(inv-cosh(x))  =  x)


By

---

Latex:
(Auto
  THEN  (D  -1  THEN  (Unhide  THENA  Auto))
  THEN  (Assert  r1  \mleq{}  (x  *  x)  BY
                          (DupHyp  (-1)  THEN  nRMul  \mkleeneopen{}x\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto  THEN  RWO  "-1<"  0  THEN  Auto))
  THEN  (Assert  r0  \mleq{}  ((x  *  x)  -  r1)  BY
                          ((RWO  "-1<"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (Assert  r0  \mleq{}  rsqrt((x  *  x)  -  r1)  BY
                          (BLemma  `rsqrt\_nonneg`  THEN  Auto))
  THEN  (Assert  r1  \mleq{}  (x  +  rsqrt((x  *  x)  -  r1))  BY
                          ((RWO  "-1<"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (Assert  r0  <  (x  +  rsqrt((x  *  x)  -  r1))  BY
                          (RWO    "-1<"  0  THEN  Auto))
  THEN  RepUR  ``cosh  inv-cosh``  0
  THEN  (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