---

Step * 1 1 1 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)/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
13. r0 ≤ arcsine(rsqrt(r1 - a * a))
14. v : ℝ
15. v = arcsine(rsqrt(r1 - a * a))
16. arcsine(rsqrt(r1 - a * a)) ∈ ℝ
17. v ∈ [r0, π/2)
18. -(π/2) < r0
19. 2 * MachinPi4() - v ∈ (r0, π/2]
20. v - 2 * MachinPi4() ∈ [-(π/2), r0)
⊢ case rless-case(r0;(r1)/2;10;a) of inl(u) => 2 * MachinPi4() - v | inr(v@0) => v - 2 * MachinPi4() ∈ {x:ℝ| 
                                                                                                        ((-(π/2) ≤ x)
                                                                                                        ∧ (x ≤ π/2))
                                                                                                        ∧ (rsin(x)
                                                                                                          = a)} 
BY
{ (GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN All Reduce
   THEN MemTypeCD
   THEN Auto
   THEN (Assert 2 * MachinPi4() = π/2 BY
               Hypothesis)
   THEN (RWO  "-1" 0 THENA Auto)) }

1
1. a : ℝ
2. r(-1) ≤ a
3. a ≤ r1
4. (r(73)/r(100)) < |a|
5. r0 ≤ (r1 - a * a)
6. rsqrt(r1 - a * a)^2 < (r(3)/r(4))^2
7. rsqrt(r1 - a * a) < (r(3)/r(4))
8. r0 ≤ rsqrt(r1 - a * a)
9. (r(-3)/r(4)) < r0
10. (r(3)/r(4)) ≤ r1
11. r(-1) < r0
12. -(π/2) < arcsine(rsqrt(r1 - a * a))
13. arcsine(rsqrt(r1 - a * a)) < π/2
14. 2 * MachinPi4() = π/2
15. r0 ≤ arcsine(rsqrt(r1 - a * a))
16. v : ℝ
17. v = arcsine(rsqrt(r1 - a * a))
18. arcsine(rsqrt(r1 - a * a)) ∈ ℝ
19. r0 ≤ v
20. v < π/2
21. -(π/2) < r0
22. r0 < (2 * MachinPi4() - v)
23. (2 * MachinPi4() - v) ≤ π/2
24. -(π/2) ≤ (v - 2 * MachinPi4())
25. (v - 2 * MachinPi4()) < r0
26. x : r0 < a
27. -(π/2) ≤ (2 * MachinPi4() - v)
28. (2 * MachinPi4() - v) ≤ π/2
29. 2 * MachinPi4() = π/2
⊢ rsin(π/2 - v) = a

2
1. a : ℝ
2. r(-1) ≤ a
3. a ≤ r1
4. (r(73)/r(100)) < |a|
5. r0 ≤ (r1 - a * a)
6. rsqrt(r1 - a * a)^2 < (r(3)/r(4))^2
7. rsqrt(r1 - a * a) < (r(3)/r(4))
8. r0 ≤ rsqrt(r1 - a * a)
9. (r(-3)/r(4)) < r0
10. (r(3)/r(4)) ≤ r1
11. r(-1) < r0
12. -(π/2) < arcsine(rsqrt(r1 - a * a))
13. arcsine(rsqrt(r1 - a * a)) < π/2
14. 2 * MachinPi4() = π/2
15. r0 ≤ arcsine(rsqrt(r1 - a * a))
16. v : ℝ
17. v = arcsine(rsqrt(r1 - a * a))
18. arcsine(rsqrt(r1 - a * a)) ∈ ℝ
19. r0 ≤ v
20. v < π/2
21. -(π/2) < r0
22. r0 < (2 * MachinPi4() - v)
23. (2 * MachinPi4() - v) ≤ π/2
24. -(π/2) ≤ (v - 2 * MachinPi4())
25. (v - 2 * MachinPi4()) < r0
26. y : a < (r1)/2
27. -(π/2) ≤ (v - 2 * MachinPi4())
28. (v - 2 * MachinPi4()) ≤ π/2
29. 2 * MachinPi4() = π/2
⊢ rsin(v - π/2) = 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)/r(4))\^{}2
6.  rsqrt(r1  -  a  *  a)  <  (r(3)/r(4))
7.  r0  \mleq{}  rsqrt(r1  -  a  *  a)
8.  (r(-3)/r(4))  <  r0
9.  (r(3)/r(4))  \mleq{}  r1
10.  r(-1)  <  r0
11.  arcsine(rsqrt(r1  -  a  *  a))  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)
12.  2  *  MachinPi4()  =  \mpi{}/2
13.  r0  \mleq{}  arcsine(rsqrt(r1  -  a  *  a))
14.  v  :  \mBbbR{}
15.  v  =  arcsine(rsqrt(r1  -  a  *  a))
16.  arcsine(rsqrt(r1  -  a  *  a))  \mmember{}  \mBbbR{}
17.  v  \mmember{}  [r0,  \mpi{}/2)
18.  -(\mpi{}/2)  <  r0
19.  2  *  MachinPi4()  -  v  \mmember{}  (r0,  \mpi{}/2]
20.  v  -  2  *  MachinPi4()  \mmember{}  [-(\mpi{}/2),  r0)
\mvdash{}  case  rless-case(r0;(r1)/2;10;a)  of  inl(u)  =>  2  *  MachinPi4()  -  v  |  inr(v@0)  =>  v  -  2  *  MachinPi4()
    \mmember{}  \{x:\mBbbR{}|  ((-(\mpi{}/2)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  \mpi{}/2))  \mwedge{}  (rsin(x)  =  a)\} 


By

---

Latex:
(GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  All  Reduce
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Assert  2  *  MachinPi4()  =  \mpi{}/2  BY
                          Hypothesis)
  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index