---

Step * 1 1 of Lemma full-arcsin_wf


1. a : ℝ
2. a ∈ [r(-1), r1]
3. x : (r(73))/100 < |a|
4. r0 ≤ (r1 - a * 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)} 
BY
{ ((RWO "int-rdiv-req" (-2)⋅ THENA Auto)
   THEN (Assert rsqrt(r1 - a * a)^2 < (r(3))/4^2 BY
               ((RWO "rsqrt-rnexp-2" 0 THENA Auto)
                THEN (Assert (r(73)/r(100))^2 < |a|^2 BY
                            (BLemma `rnexp-rless` THEN Auto))
                THEN (Assert |a|^2 = (a * a) BY
                            ((RWW "rnexp2 rabs-rmul<" 0 THEN Auto) THEN RWO  "rabs-of-nonneg" 0 THEN Auto))
                THEN (RWO "-1" (-2) THENA Auto)
                THEN (RWO "-2<" 0 THENA Auto)
                THEN D 0 With ⌜1000⌝ 
                THEN Computation
                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))/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)} 

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  a  \mmember{}  [r(-1),  r1]
3.  x  :  (r(73))/100  <  |a|
4.  r0  \mleq{}  (r1  -  a  *  a)
\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"  (-2)\mcdot{}  THENA  Auto)
  THEN  (Assert  rsqrt(r1  -  a  *  a)\^{}2  <  (r(3))/4\^{}2  BY
                          ((RWO  "rsqrt-rnexp-2"  0  THENA  Auto)
                            THEN  (Assert  (r(73)/r(100))\^{}2  <  |a|\^{}2  BY
                                                    (BLemma  `rnexp-rless`  THEN  Auto))
                            THEN  (Assert  |a|\^{}2  =  (a  *  a)  BY
                                                    ((RWW  "rnexp2  rabs-rmul<"  0  THEN  Auto)
                                                      THEN  RWO    "rabs-of-nonneg"  0
                                                      THEN  Auto))
                            THEN  (RWO  "-1"  (-2)  THENA  Auto)
                            THEN  (RWO  "-2<"  0  THENA  Auto)
                            THEN  D  0  With  \mkleeneopen{}1000\mkleeneclose{} 
                            THEN  Computation
                            THEN  Auto))
  )

---

Home Index