---

Step * of Lemma arcsine-nonneg

∀[x:{x:ℝ| x ∈ [r0, r1)} ]. (r0 ≤ arcsine(x))
BY
{ (Intro
   THEN (Assert x ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)}  BY
               (MemTypeCD THEN Auto THEN D 1 THEN Unhide THEN Reduce -1 THEN Auto THEN RWO "2<" 0⋅ THEN Auto))
   ) }

1
1. [x] : {x:ℝ| x ∈ [r0, r1)} 
2. x ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
⊢ r0 ≤ arcsine(x)

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1)\}  ].  (r0  \mleq{}  arcsine(x))


By

---

Latex:
(Intro
  THEN  (Assert  x  \mmember{}  \{x:\mBbbR{}|  (r(-1)  <  x)  \mwedge{}  (x  <  r1)\}    BY
                          (MemTypeCD
                            THEN  Auto
                            THEN  D  1
                            THEN  Unhide
                            THEN  Reduce  -1
                            THEN  Auto
                            THEN  RWO  "2<"  0\mcdot{}
                            THEN  Auto))
  )

---

Home Index