---

Step * 1 1 1 of Lemma rsin-arcsine


1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. [rmin(rsin(arcsine(x));r0), rmax(rsin(arcsine(x));r0)] ⊆ (r(-1), r1) 
3. [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1) 
4. x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx = (x_∫-r0 arcsine_deriv(x) dx + arcsine(rsin(arcsine(x))))
⊢ rsin(arcsine(x)) = x
BY
{ ((Assert [rmin(x;r0), rmax(x;r0)] ⊆ (r(-1), r1)  BY
          (D 0
           THEN Reduce 0
           THEN Auto
           THEN Try (((RWO "-2<" 0 THEN Auto) THEN BLemma `rmin_strict_ub` THEN Auto))
           THEN (RWO  "-2" 0 THENA Auto)
           THEN BLemma `rmax_strict_lb`
           THEN Auto))
   THEN (Assert x_∫-r0 arcsine_deriv(x) dx = -(r0_∫-x arcsine_deriv(x) dx) BY
               (BLemma `integral-reverse` THEN Auto THEN Try ((RWO "-1" 0 THEN Auto))))
   ) }

1
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. [rmin(rsin(arcsine(x));r0), rmax(rsin(arcsine(x));r0)] ⊆ (r(-1), r1) 
3. [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1) 
4. x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx = (x_∫-r0 arcsine_deriv(x) dx + arcsine(rsin(arcsine(x))))
5. [rmin(x;r0), rmax(x;r0)] ⊆ (r(-1), r1) 
6. x_∫-r0 arcsine_deriv(x) dx = -(r0_∫-x arcsine_deriv(x) dx)
⊢ rsin(arcsine(x)) = x

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\} 
2.  [rmin(rsin(arcsine(x));r0),  rmax(rsin(arcsine(x));r0)]  \msubseteq{}  (r(-1),  r1) 
3.  [rmin(x;rmin(rsin(arcsine(x));r0)),  rmax(x;rmax(rsin(arcsine(x));r0))]  \msubseteq{}  (r(-1),  r1) 
4.  x\_\mint{}\msupminus{}rsin(arcsine(x))  arcsine\_deriv(x)  dx
=  (x\_\mint{}\msupminus{}r0  arcsine\_deriv(x)  dx  +  arcsine(rsin(arcsine(x))))
\mvdash{}  rsin(arcsine(x))  =  x


By

---

Latex:
((Assert  [rmin(x;r0),  rmax(x;r0)]  \msubseteq{}  (r(-1),  r1)    BY
                (D  0
                  THEN  Reduce  0
                  THEN  Auto
                  THEN  Try  (((RWO  "-2<"  0  THEN  Auto)  THEN  BLemma  `rmin\_strict\_ub`  THEN  Auto))
                  THEN  (RWO    "-2"  0  THENA  Auto)
                  THEN  BLemma  `rmax\_strict\_lb`
                  THEN  Auto))
  THEN  (Assert  x\_\mint{}\msupminus{}r0  arcsine\_deriv(x)  dx  =  -(r0\_\mint{}\msupminus{}x  arcsine\_deriv(x)  dx)  BY
                          (BLemma  `integral-reverse`  THEN  Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto))))
  )

---

Home Index