---

Step * of Lemma arcsine-shift

∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. arcsine(x) = (π/2 - arcsine(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 (Unhide THENA Auto)
   THEN (Assert (r1 - x * x) < r1 BY
               (nRAdd ⌜(x * x) - r1⌝ 0⋅ THEN Auto THEN BLemma `rmul-is-positive` THEN Auto))
   THEN FLemma `rsqrt_functionality_wrt_rless` [-1]
   THEN Auto
   THEN (RWO "rsqrt1" (-1) THENA Auto)
   THEN (Assert rsqrt(r1 - x * x) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)}  BY
               ((MemTypeCD THEN Auto) THEN (Assert r0 ≤ rsqrt(r1 - x * x) BY Auto) THEN RWO  "-1<" 0 THEN Auto))
   THEN (Auto THEN BLemma `arcsine-unique`)
   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. rsqrt(r1 - x * x) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
⊢ π/2 - arcsine(rsqrt(r1 - x * x)) ∈ {y:ℝ| (-(π/2) < y) ∧ (y < π/2)} 

2
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. rsqrt(r1 - x * x) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
⊢ rsin(π/2 - arcsine(rsqrt(r1 - x * x))) = x

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  ].  arcsine(x)  =  (\mpi{}/2  -  arcsine(rsqrt(r1  -  x  *  x)))  supposing  r0  <  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  (Unhide  THENA  Auto)
  THEN  (Assert  (r1  -  x  *  x)  <  r1  BY
                          (nRAdd  \mkleeneopen{}(x  *  x)  -  r1\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  BLemma  `rmul-is-positive`  THEN  Auto))
  THEN  FLemma  `rsqrt\_functionality\_wrt\_rless`  [-1]
  THEN  Auto
  THEN  (RWO  "rsqrt1"  (-1)  THENA  Auto)
  THEN  (Assert  rsqrt(r1  -  x  *  x)  \mmember{}  \{x:\mBbbR{}|  (r(-1)  <  x)  \mwedge{}  (x  <  r1)\}    BY
                          ((MemTypeCD  THEN  Auto)
                            THEN  (Assert  r0  \mleq{}  rsqrt(r1  -  x  *  x)  BY
                                                    Auto)
                            THEN  RWO    "-1<"  0
                            THEN  Auto))
  THEN  (Auto  THEN  BLemma  `arcsine-unique`)
  THEN  Auto)

---

Home Index