---

Step * 1 1 of Lemma arcsine-bounds2

.....antecedent..... 
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
⊢ d(arcsine(x) - x)/dx = λx.arcsine_deriv(x) - r1 on [r0, (r(3)/r(4))]
BY
{ (ProveDerivative THEN Auto THEN Try ((D -1 THEN Reduce -1 THEN MemTypeCD THEN Auto))) }

1
1. x : {x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} 
2. r(-1) < r0
3. (r(3)/r(4)) < r1
⊢ d(arcsine(x))/dx = λx.arcsine_deriv(x) on [r0, (r(3)/r(4))]

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \{x:\mBbbR{}|  (r0  <  x)  \mwedge{}  (x  <  (r(3)/r(4)))\} 
2.  r(-1)  <  r0
3.  (r(3)/r(4))  <  r1
\mvdash{}  d(arcsine(x)  -  x)/dx  =  \mlambda{}x.arcsine\_deriv(x)  -  r1  on  [r0,  (r(3)/r(4))]


By

---

Latex:
(ProveDerivative  THEN  Auto  THEN  Try  ((D  -1  THEN  Reduce  -1  THEN  MemTypeCD  THEN  Auto)))

---

Home Index