---

Step * of Lemma arccos_wf

∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arccos(a) ∈ {x:ℝ| (x ∈ [r0, π]) ∧ (rcos(x) = a)} )
BY
{ (InstLemma `arcsin_wf` []
   THEN (ParallelLast' THEN (MemTypeHD (-1) THENA Auto))
   THEN Reduce -1
   THEN ProveWfLemma
   THEN Unfold `pi` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((RWO "int-rmul-req" 0 THEN Auto))) }

1
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

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  a  \mmember{}  [r(-1),  r1]\}  ].  (arccos(a)  \mmember{}  \{x:\mBbbR{}|  (x  \mmember{}  [r0,  \mpi{}])  \mwedge{}  (rcos(x)  =  a)\}  )


By

---

Latex:
(InstLemma  `arcsin\_wf`  []
  THEN  (ParallelLast'  THEN  (MemTypeHD  (-1)  THENA  Auto))
  THEN  Reduce  -1
  THEN  ProveWfLemma
  THEN  Unfold  `pi`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((RWO  "int-rmul-req"  0  THEN  Auto)))

---

Home Index