---

Step * 2 of Lemma full-arcsin_wf


1. a : ℝ
2. a ∈ [r(-1), r1]
3. y : |a| < (r(3))/4
⊢ partial-arcsin(a) ∈ {x:ℝ| ((-(π/2) ≤ x) ∧ (x ≤ π/2)) ∧ (rsin(x) = a)} 
BY
{ (((RWO "rabs-rless-iff" (-1) THENA Auto) THEN (All (RWO "int-rdiv-req") THENA Auto)) THEN DoSubsume) }

1
1. a : ℝ
2. a ∈ [r(-1), r1]
3. (-((r(3)/r(4))) < a) ∧ (a < (r(3)/r(4)))
⊢ partial-arcsin(a) ∈ {x:ℝ| x = arcsine(a)} 

2
1. a : ℝ
2. a ∈ [r(-1), r1]
3. (-((r(3)/r(4))) < a) ∧ (a < (r(3)/r(4)))
4. partial-arcsin(a) = partial-arcsin(a) ∈ {x:ℝ| x = arcsine(a)} 
⊢ {x:ℝ| x = arcsine(a)}  ⊆r {x:ℝ| ((-(π/2) ≤ x) ∧ (x ≤ π/2)) ∧ (rsin(x) = a)} 

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  a  \mmember{}  [r(-1),  r1]
3.  y  :  |a|  <  (r(3))/4
\mvdash{}  partial-arcsin(a)  \mmember{}  \{x:\mBbbR{}|  ((-(\mpi{}/2)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  \mpi{}/2))  \mwedge{}  (rsin(x)  =  a)\} 


By

---

Latex:
(((RWO  "rabs-rless-iff"  (-1)  THENA  Auto)  THEN  (All  (RWO  "int-rdiv-req")  THENA  Auto))  THEN  DoSubsume)

---

Home Index