---

Step * of Lemma full-arcsin_wf

∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (full-arcsin(a) ∈ {x:ℝ| (x ∈ [-(π/2), π/2]) ∧ (rsin(x) = a)} )
BY
{ (Intros
   THEN Unhide
   THEN D -1
   THEN Unhide
   THEN Unfold `full-arcsin` 0
   THEN GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0) }

1
1. a : ℝ
2. a ∈ [r(-1), r1]
3. x : (r(73))/100 < |a|
⊢ case rless-case(r0;(r1)/2;10;a)
   of inl(u) =>
   2 * MachinPi4() - partial-arcsin(rsqrt(r1 - a * a))
   | inr(v) =>
   partial-arcsin(rsqrt(r1 - a * a)) - 2 * MachinPi4() ∈ {x:ℝ| ((-(π/2) ≤ x) ∧ (x ≤ π/2)) ∧ (rsin(x) = a)} 

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

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  a  \mmember{}  [r(-1),  r1]\}  ].  (full-arcsin(a)  \mmember{}  \{x:\mBbbR{}|  (x  \mmember{}  [-(\mpi{}/2),  \mpi{}/2])  \mwedge{}  (rsin(x)  =  a)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  -1
  THEN  Unhide
  THEN  Unfold  `full-arcsin`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index