---

Step * 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) 
⊢ rsin(arcsine(x)) = x
BY
{ (Assert [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1)  BY
         (D 0
          THEN Reduce 0
          THEN Auto
          THEN Try (((RWO "-2" 0 THENA Auto) THEN BLemma `rmax_strict_lb` THEN Auto))
          THEN Try (((RWO "-2<" 0 THENA Auto) THEN BLemma `rmin_strict_ub` 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) 
⊢ 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) 
\mvdash{}  rsin(arcsine(x))  =  x


By

---

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

---

Home Index