---

Step * of Lemma arccos_functionality

∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[x':ℝ].  arccos(x) = arccos(x') supposing x = x'
BY
{ (Intros
   THEN (Assert x' ∈ {a:ℝ| (r(-1) ≤ a) ∧ (a ≤ r1)}  BY
               (Unhide THEN DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))
   THEN Unfold `arccos` 0
   THEN Unhide
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (Assert  x'  \mmember{}  \{a:\mBbbR{}|  (r(-1)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  r1)\}    BY
                          (Unhide  THEN  DSetVars  THEN  All  Reduce  THEN  MemTypeCD  THEN  Auto))
  THEN  Unfold  `arccos`  0
  THEN  Unhide
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index