---

Step * of Lemma arcsine_deriv_functionality

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. ∀[y:ℝ].  arcsine_deriv(x) = arcsine_deriv(y) supposing x = y
BY
{ (InstLemma `arcsine-root-bounds` []
   THEN (Auto THEN DSetVars THEN All Reduce THEN Auto)
   THEN (Unhide THENA Auto)
   THEN (Assert r0 < (r1 - x * x) BY
               Auto)
   THEN (Assert r0 < (r1 - y * y) BY
               Auto)) }

1
1. ∀t:ℝ. (((r(-1) < t) ∧ (t < r1)) ⇒ (r0 < (r1 - t * t)))
2. x : ℝ
3. (r(-1) < x) ∧ (x < r1)
4. y : ℝ
5. x = y
6. r0 < (r1 - x * x)
7. r0 < (r1 - y * y)
⊢ arcsine_deriv(x) = arcsine_deriv(y)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `arcsine-root-bounds`  []
  THEN  (Auto  THEN  DSetVars  THEN  All  Reduce  THEN  Auto)
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  r0  <  (r1  -  x  *  x)  BY
                          Auto)
  THEN  (Assert  r0  <  (r1  -  y  *  y)  BY
                          Auto))

---

Home Index