---

Step * of Lemma cosh-gt-1

∀x:ℝ. (x ≠ r0 ⇒ (r1 < cosh(x)))
BY
{ (Auto THEN RepUR ``cosh`` 0 THEN (RWW "int-rdiv-req expr-req" 0 THENA Auto) THEN (nRMul ⌜r(2)⌝ 0⋅ THENA Auto)) }

1
1. x : ℝ
2. x ≠ r0
⊢ r(2) < (e^-(x) + e^x)

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (x  \mneq{}  r0  {}\mRightarrow{}  (r1  <  cosh(x)))


By

---

Latex:
(Auto
  THEN  RepUR  ``cosh``  0
  THEN  (RWW  "int-rdiv-req  expr-req"  0  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index