---

Step * of Lemma cosh-ge-1

∀[x:ℝ]. (r1 ≤ cosh(x))
BY
{ (Auto
   THEN (Assert r0 ≤ sinh(x)^2 BY
               Auto)
   THEN (Assert r1 ≤ cosh(x)^2 BY
               (nRAdd ⌜-(sinh(x)^2)⌝ 0⋅ THEN Fold `rsub` 0 THEN RWO "cosh2-sinh2" 0 THEN Auto))) }

1
1. x : ℝ
2. r0 ≤ sinh(x)^2
3. r1 ≤ cosh(x)^2
⊢ r1 ≤ cosh(x)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  r0  \mleq{}  sinh(x)\^{}2  BY
                          Auto)
  THEN  (Assert  r1  \mleq{}  cosh(x)\^{}2  BY
                          (nRAdd  \mkleeneopen{}-(sinh(x)\^{}2)\mkleeneclose{}  0\mcdot{}  THEN  Fold  `rsub`  0  THEN  RWO  "cosh2-sinh2"  0  THEN  Auto)))

---

Home Index