---

Step * of Lemma arcsin-minus1

arcsin(r(-1)) = -(π/2)
BY
{ ((Assert -(r1) ∈ {a:ℝ| (r(-1) ≤ a) ∧ (a ≤ r1)}  BY
          ((MemTypeCD THEN Auto) THEN nRNorm 0 THEN Auto))
   THEN (RWO "arcsin1<" 0 THENA Auto)
   THEN (RWO "arcsin-rminus<" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
arcsin(r(-1))  =  -(\mpi{}/2)


By

---

Latex:
((Assert  -(r1)  \mmember{}  \{a:\mBbbR{}|  (r(-1)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  r1)\}    BY
                ((MemTypeCD  THEN  Auto)  THEN  nRNorm  0  THEN  Auto))
  THEN  (RWO  "arcsin1<"  0  THENA  Auto)
  THEN  (RWO  "arcsin-rminus<"  0  THENA  Auto))

---

Home Index