---

Step * of Lemma arcsine-rminus

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsine(-(x)) = -(arcsine(x)))
BY
{ (Intro
   THEN (Assert -(x) ∈ {x:ℝ| x ∈ (r(-1), r1)}  BY
               (Unhide
                THEN D 1
                THEN Reduce 2
                THEN MemTypeCD
                THEN Reduce 0
                THEN Auto
                THEN (FLemma `rminus-reverses-rless` [-1] THEN Auto)
                THEN FLemma `rminus-reverses-rless` [2]
                THEN Auto))
   ) }

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

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  (Assert  -(x)  \mmember{}  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}    BY
                          (Unhide
                            THEN  D  1
                            THEN  Reduce  2
                            THEN  MemTypeCD
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (FLemma  `rminus-reverses-rless`  [-1]  THEN  Auto)
                            THEN  FLemma  `rminus-reverses-rless`  [2]
                            THEN  Auto))
  )

---

Home Index