---

Step * of Lemma arcsine_deriv_wf

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsine_deriv(x) ∈ ℝ)
BY
{ (InstLemma `arcsine-root-bounds` [] THEN Auto THEN (Assert r0 < (r1 - x * x) BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  ].  (arcsine\_deriv(x)  \mmember{}  \mBbbR{})


By

---

Latex:
(InstLemma  `arcsine-root-bounds`  []
  THEN  Auto
  THEN  (Assert  r0  <  (r1  -  x  *  x)  BY
                          Auto)
  THEN  ProveWfLemma)

---

Home Index