---

Step * of Lemma arcsin-rminus

∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arcsin(-(a)) = -(arcsin(a)))
BY
{ (Intro
   THEN (Assert -(a) ∈ {a:ℝ| (r(-1) ≤ a) ∧ (a ≤ r1)}  BY
               ((MemTypeCD THEN Auto) THEN DSetVars THEN Unhide THEN Auto THEN All Reduce THEN Auto))
   ) }

1
1. [a] : {a:ℝ| a ∈ [r(-1), r1]} 
2. -(a) ∈ {a:ℝ| (r(-1) ≤ a) ∧ (a ≤ r1)} 
⊢ arcsin(-(a)) = -(arcsin(a))

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  (Assert  -(a)  \mmember{}  \{a:\mBbbR{}|  (r(-1)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  r1)\}    BY
                          ((MemTypeCD  THEN  Auto)  THEN  DSetVars  THEN  Unhide  THEN  Auto  THEN  All  Reduce  THEN  Auto))
  )

---

Home Index