---

Step * 1 1 1 1 1 1 1 of Lemma full-arcsin_wf


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
BY
{ (StableCases ⌜a < r1⌝⋅ 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
30. a < r1
⊢ 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. x : r0 < a
27. -(π/2) ≤ (2 * MachinPi4() - v)
28. (2 * MachinPi4() - v) ≤ π/2
29. 2 * MachinPi4() = π/2
30. ¬(a < r1)
⊢ rsin(π/2 - v) = a

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  r(-1)  \mleq{}  a
3.  a  \mleq{}  r1
4.  (r(73)/r(100))  <  |a|
5.  r0  \mleq{}  (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  \mleq{}  rsqrt(r1  -  a  *  a)
9.  (r(-3)/r(4))  <  r0
10.  (r(3)/r(4))  \mleq{}  r1
11.  r(-1)  <  r0
12.  -(\mpi{}/2)  <  arcsine(rsqrt(r1  -  a  *  a))
13.  arcsine(rsqrt(r1  -  a  *  a))  <  \mpi{}/2
14.  2  *  MachinPi4()  =  \mpi{}/2
15.  r0  \mleq{}  arcsine(rsqrt(r1  -  a  *  a))
16.  v  :  \mBbbR{}
17.  v  =  arcsine(rsqrt(r1  -  a  *  a))
18.  arcsine(rsqrt(r1  -  a  *  a))  \mmember{}  \mBbbR{}
19.  r0  \mleq{}  v
20.  v  <  \mpi{}/2
21.  -(\mpi{}/2)  <  r0
22.  r0  <  (2  *  MachinPi4()  -  v)
23.  (2  *  MachinPi4()  -  v)  \mleq{}  \mpi{}/2
24.  -(\mpi{}/2)  \mleq{}  (v  -  2  *  MachinPi4())
25.  (v  -  2  *  MachinPi4())  <  r0
26.  x  :  r0  <  a
27.  -(\mpi{}/2)  \mleq{}  (2  *  MachinPi4()  -  v)
28.  (2  *  MachinPi4()  -  v)  \mleq{}  \mpi{}/2
29.  2  *  MachinPi4()  =  \mpi{}/2
\mvdash{}  rsin(\mpi{}/2  -  v)  =  a


By

---

Latex:
(StableCases  \mkleeneopen{}a  <  r1\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index