---

Step * 1 1 1 of Lemma full-arcsin_wf


1. a : ℝ
2. a ∈ [r(-1), r1]
3. (r(73)/r(100)) < |a|
4. r0 ≤ (r1 - a * a)
5. rsqrt(r1 - a * a)^2 < (r(3))/4^2
⊢ 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)} 
BY
{ ((RWO "int-rdiv-req" (-1) THENA Auto)
   THEN (FLemma `square-rless-implies` [-1] THENA Auto)
   THEN (Assert r0 ≤ rsqrt(r1 - a * a) BY
               Auto)
   THEN (Assert (r(-3)/r(4)) < r0 BY
               Auto)
   THEN (Assert (r(3)/r(4)) ≤ r1 BY
               Auto)
   THEN (Assert r(-1) < r0 BY
               Auto)
   THEN (InstLemma `arcsine-bounds` [⌜rsqrt(r1 - a * a)⌝]⋅ THENA (MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (Assert 2 * MachinPi4() = π/2 BY
               ((GenConclTerm ⌜MachinPi4()⌝⋅ THENA Auto)
                THEN (Thin (-1) THEN D -1)
                THEN (Unhide THENA Auto)
                THEN ((RWO "-1" 0 THEN Auto) THEN Unfold `pi` 0)
                THEN RWW "int-rmul-req" 0
                THEN Auto))) }

1
1. a : ℝ
2. a ∈ [r(-1), r1]
3. (r(73)/r(100)) < |a|
4. r0 ≤ (r1 - a * a)
5. rsqrt(r1 - a * a)^2 < (r(3)/r(4))^2
6. rsqrt(r1 - a * a) < (r(3)/r(4))
7. r0 ≤ rsqrt(r1 - a * a)
8. (r(-3)/r(4)) < r0
9. (r(3)/r(4)) ≤ r1
10. r(-1) < r0
11. arcsine(rsqrt(r1 - a * a)) ∈ (-(π/2), π/2)
12. 2 * MachinPi4() = π/2
⊢ 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)} 

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  a  \mmember{}  [r(-1),  r1]
3.  (r(73)/r(100))  <  |a|
4.  r0  \mleq{}  (r1  -  a  *  a)
5.  rsqrt(r1  -  a  *  a)\^{}2  <  (r(3))/4\^{}2
\mvdash{}  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()  \mmember{}  \{x:\mBbbR{}| 
                                                                                                                    ((-(\mpi{}/2)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  \mpi{}/2))
                                                                                                                    \mwedge{}  (rsin(x)  =  a)\} 


By

---

Latex:
((RWO  "int-rdiv-req"  (-1)  THENA  Auto)
  THEN  (FLemma  `square-rless-implies`  [-1]  THENA  Auto)
  THEN  (Assert  r0  \mleq{}  rsqrt(r1  -  a  *  a)  BY
                          Auto)
  THEN  (Assert  (r(-3)/r(4))  <  r0  BY
                          Auto)
  THEN  (Assert  (r(3)/r(4))  \mleq{}  r1  BY
                          Auto)
  THEN  (Assert  r(-1)  <  r0  BY
                          Auto)
  THEN  (InstLemma  `arcsine-bounds`  [\mkleeneopen{}rsqrt(r1  -  a  *  a)\mkleeneclose{}]\mcdot{}  THENA  (MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  2  *  MachinPi4()  =  \mpi{}/2  BY
                          ((GenConclTerm  \mkleeneopen{}MachinPi4()\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (Thin  (-1)  THEN  D  -1)
                            THEN  (Unhide  THENA  Auto)
                            THEN  ((RWO  "-1"  0  THEN  Auto)  THEN  Unfold  `pi`  0)
                            THEN  RWW  "int-rmul-req"  0
                            THEN  Auto)))

---

Home Index