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 0 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