---

Step * 1 1 1 of Lemma arcsine-bounds2


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))]
BY
{ (InstLemma `derivative-arcsine` []
   THEN (Assert [r0, (r(3)/r(4))] ⊆ (r(-1), r1)  BY
               (D 0 THEN Reduce 0 THEN Auto))
   THEN FLemma `derivative_functionality_wrt_subinterval` [-1;-2]
   THEN Auto) }

---

Latex:

---

Latex:

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))/dx  =  \mlambda{}x.arcsine\_deriv(x)  on  [r0,  (r(3)/r(4))]


By

---

Latex:
(InstLemma  `derivative-arcsine`  []
  THEN  (Assert  [r0,  (r(3)/r(4))]  \msubseteq{}  (r(-1),  r1)    BY
                          (D  0  THEN  Reduce  0  THEN  Auto))
  THEN  FLemma  `derivative\_functionality\_wrt\_subinterval`  [-1;-2]
  THEN  Auto)

---

Home Index