---

Step * of Lemma inv-cosh_wf

∀[x:{x:ℝ| r1 ≤ x} ]. (inv-cosh(x) ∈ ℝ)
BY
{ (Auto
   THEN D -1
   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 ProveWfLemma) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -1
  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  ProveWfLemma)

---

Home Index