---

Step * of Lemma rsin-arcsine

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (rsin(arcsine(x)) = x)
BY
{ (Auto
   THEN (InstLemma `rmin-rmax-subinterval` 
         [⌜(r(-1), r1)⌝;⌜rsin(arcsine(x))⌝;⌜r0⌝]⋅
         THENA (Auto THEN BLemma `rsin-strict-bound` THEN Auto)
         )
   ) }

1
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

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  ].  (rsin(arcsine(x))  =  x)


By

---

Latex:
(Auto
  THEN  (InstLemma  `rmin-rmax-subinterval` 
              [\mkleeneopen{}(r(-1),  r1)\mkleeneclose{};\mkleeneopen{}rsin(arcsine(x))\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `rsin-strict-bound`  THEN  Auto)
              )
  )

---

Home Index