---

Step * of Lemma arcsin-shift

∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. arcsin(x) = (π/2 - arcsin(rsqrt(r1 - x * x))) supposing r0 ≤ x
BY
{ (Intro
   THEN (Assert r0 ≤ (r1 - x * x) BY
               (nRAdd ⌜x * x⌝ 0⋅
                THEN D 1
                THEN ((Unhide THENA Auto) THEN Reduce -1)
                THEN RWW  "rnexp2< square-rleq-1-iff rabs-rleq-iff" 0
                THEN Auto
                THEN RWO "rminus-int" 0
                THEN Auto))
   THEN Intro
   THEN (Assert (r1 - x * x) ≤ r1 BY
               (nRAdd ⌜(x * x) - r1⌝ 0⋅ THEN Auto))
   THEN FLemma `rsqrt_functionality_wrt_rleq` [-1]
   THEN Auto
   THEN (RWO "rsqrt1" (-1) THENA Auto)
   THEN (Assert r0 ≤ rsqrt(r1 - x * x) BY
               Auto)
   THEN (Assert r(-1) ≤ r0 BY
               Auto)
   THEN (Assert arcsin(rsqrt(r1 - x * x)) ∈ ℝ BY
               (MemCD THEN MemTypeCD THEN Reduce 0 THEN Auto))) }

1
1. [x] : {x:ℝ| x ∈ [r(-1), r1]} 
2. r0 ≤ (r1 - x * x)
3. [%] : r0 ≤ x
4. (r1 - x * x) ≤ r1
5. rsqrt(r1 - x * x) ≤ r1
6. r0 ≤ rsqrt(r1 - x * x)
7. r(-1) ≤ r0
8. arcsin(rsqrt(r1 - x * x)) ∈ ℝ
⊢ arcsin(x) = (π/2 - arcsin(rsqrt(r1 - x * x)))

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  [r(-1),  r1]\}  ].  arcsin(x)  =  (\mpi{}/2  -  arcsin(rsqrt(r1  -  x  *  x)))  supposing  r0  \mleq{}  x


By

---

Latex:
(Intro
  THEN  (Assert  r0  \mleq{}  (r1  -  x  *  x)  BY
                          (nRAdd  \mkleeneopen{}x  *  x\mkleeneclose{}  0\mcdot{}
                            THEN  D  1
                            THEN  ((Unhide  THENA  Auto)  THEN  Reduce  -1)
                            THEN  RWW    "rnexp2<  square-rleq-1-iff  rabs-rleq-iff"  0
                            THEN  Auto
                            THEN  RWO  "rminus-int"  0
                            THEN  Auto))
  THEN  Intro
  THEN  (Assert  (r1  -  x  *  x)  \mleq{}  r1  BY
                          (nRAdd  \mkleeneopen{}(x  *  x)  -  r1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  FLemma  `rsqrt\_functionality\_wrt\_rleq`  [-1]
  THEN  Auto
  THEN  (RWO  "rsqrt1"  (-1)  THENA  Auto)
  THEN  (Assert  r0  \mleq{}  rsqrt(r1  -  x  *  x)  BY
                          Auto)
  THEN  (Assert  r(-1)  \mleq{}  r0  BY
                          Auto)
  THEN  (Assert  arcsin(rsqrt(r1  -  x  *  x))  \mmember{}  \mBbbR{}  BY
                          (MemCD  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)))

---

Home Index