---

Step * 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) 
⊢ rsin(arcsine(x)) = x
BY
{ ((InstLemma `integral-additive` 
    [⌜x⌝;⌜rsin(arcsine(x))⌝;⌜r0⌝;⌜λ2x.arcsine_deriv(x)⌝]⋅
    THENA (Auto THEN Try ((RWO  "-1" 0 THEN Auto)) THEN Try (((BLemma `rmin_lb` THENM OrLeft) THEN Auto)))
    )
   THEN Fold `arcsine` (-1)
   ) }

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))))
⊢ 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) 
\mvdash{}  rsin(arcsine(x))  =  x


By

---

Latex:
((InstLemma  `integral-additive` 
    [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}rsin(arcsine(x))\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine\_deriv(x)\mkleeneclose{}]\mcdot{}
    THENA  (Auto
                  THEN  Try  ((RWO    "-1"  0  THEN  Auto))
                  THEN  Try  (((BLemma  `rmin\_lb`  THENM  OrLeft)  THEN  Auto)))
    )
  THEN  Fold  `arcsine`  (-1)
  )

---

Home Index