---

Step * 1 of Lemma arccos_wf


1. a : ℝ
2. a ∈ [r(-1), r1]
3. arcsin(a) = arcsin(a) ∈ ℝ
4. -(π/2) ≤ arcsin(a)
5. arcsin(a) ≤ π/2
6. rsin(arcsin(a)) = a
7. r0 ≤ (π/2 - arcsin(a))
8. (π/2 - arcsin(a)) ≤ 2 * π/2
⊢ rcos(π/2 - arcsin(a)) = a
BY
{ ((Assert -(a) ∈ [r(-1), r1] BY
          (All Reduce THEN Auto))
   THEN (Assert (π/2 - arcsin(a)) = (arcsin(-(a)) + π/2) BY
               (RWO "arcsin-rminus" 0 THEN Auto))
   THEN RWW "-1 rcos-shift-half-pi rsin-arcsin" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  a  \mmember{}  [r(-1),  r1]
3.  arcsin(a)  =  arcsin(a)
4.  -(\mpi{}/2)  \mleq{}  arcsin(a)
5.  arcsin(a)  \mleq{}  \mpi{}/2
6.  rsin(arcsin(a))  =  a
7.  r0  \mleq{}  (\mpi{}/2  -  arcsin(a))
8.  (\mpi{}/2  -  arcsin(a))  \mleq{}  2  *  \mpi{}/2
\mvdash{}  rcos(\mpi{}/2  -  arcsin(a))  =  a


By

---

Latex:
((Assert  -(a)  \mmember{}  [r(-1),  r1]  BY
                (All  Reduce  THEN  Auto))
  THEN  (Assert  (\mpi{}/2  -  arcsin(a))  =  (arcsin(-(a))  +  \mpi{}/2)  BY
                          (RWO  "arcsin-rminus"  0  THEN  Auto))
  THEN  RWW  "-1  rcos-shift-half-pi  rsin-arcsin"  0
  THEN  Auto)

---

Home Index