Step * 1 of Lemma arcsin-bounds


1. [a] {a:ℝa ∈ [r(-1), r1]} 
2. arcsin(a) arcsin(a) ∈ ℝ
3. [%] (arcsin(a) ∈ [-(π/2), π/2]) ∧ (rsin(arcsin(a)) a)
⊢ SqStable(arcsin(a) ∈ [-(π/2), π/2])
BY
(Reduce THEN Auto) }


Latex:


Latex:

1.  [a]  :  \{a:\mBbbR{}|  a  \mmember{}  [r(-1),  r1]\} 
2.  arcsin(a)  =  arcsin(a)
3.  [\%]  :  (arcsin(a)  \mmember{}  [-(\mpi{}/2),  \mpi{}/2])  \mwedge{}  (rsin(arcsin(a))  =  a)
\mvdash{}  SqStable(arcsin(a)  \mmember{}  [-(\mpi{}/2),  \mpi{}/2])


By


Latex:
(Reduce  0  THEN  Auto)




Home Index