Step |
Hyp |
Ref |
Expression |
1 |
|
neghalfpire |
⊢ - ( π / 2 ) ∈ ℝ |
2 |
1
|
rexri |
⊢ - ( π / 2 ) ∈ ℝ* |
3 |
|
halfpire |
⊢ ( π / 2 ) ∈ ℝ |
4 |
3
|
rexri |
⊢ ( π / 2 ) ∈ ℝ* |
5 |
|
pirp |
⊢ π ∈ ℝ+ |
6 |
|
rphalfcl |
⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ ) |
7 |
5 6
|
ax-mp |
⊢ ( π / 2 ) ∈ ℝ+ |
8 |
|
rpgt0 |
⊢ ( ( π / 2 ) ∈ ℝ+ → 0 < ( π / 2 ) ) |
9 |
7 8
|
ax-mp |
⊢ 0 < ( π / 2 ) |
10 |
|
lt0neg2 |
⊢ ( ( π / 2 ) ∈ ℝ → ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) ) |
11 |
3 10
|
ax-mp |
⊢ ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) |
12 |
9 11
|
mpbi |
⊢ - ( π / 2 ) < 0 |
13 |
|
0re |
⊢ 0 ∈ ℝ |
14 |
1 13 3
|
lttri |
⊢ ( ( - ( π / 2 ) < 0 ∧ 0 < ( π / 2 ) ) → - ( π / 2 ) < ( π / 2 ) ) |
15 |
12 9 14
|
mp2an |
⊢ - ( π / 2 ) < ( π / 2 ) |
16 |
1 3 15
|
ltleii |
⊢ - ( π / 2 ) ≤ ( π / 2 ) |
17 |
|
prunioo |
⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ - ( π / 2 ) ≤ ( π / 2 ) ) → ( ( - ( π / 2 ) (,) ( π / 2 ) ) ∪ { - ( π / 2 ) , ( π / 2 ) } ) = ( - ( π / 2 ) [,] ( π / 2 ) ) ) |
18 |
2 4 16 17
|
mp3an |
⊢ ( ( - ( π / 2 ) (,) ( π / 2 ) ) ∪ { - ( π / 2 ) , ( π / 2 ) } ) = ( - ( π / 2 ) [,] ( π / 2 ) ) |
19 |
18
|
eleq2i |
⊢ ( 𝐴 ∈ ( ( - ( π / 2 ) (,) ( π / 2 ) ) ∪ { - ( π / 2 ) , ( π / 2 ) } ) ↔ 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) |
20 |
|
elun |
⊢ ( 𝐴 ∈ ( ( - ( π / 2 ) (,) ( π / 2 ) ) ∪ { - ( π / 2 ) , ( π / 2 ) } ) ↔ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∨ 𝐴 ∈ { - ( π / 2 ) , ( π / 2 ) } ) ) |
21 |
19 20
|
bitr3i |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∨ 𝐴 ∈ { - ( π / 2 ) , ( π / 2 ) } ) ) |
22 |
|
elioore |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℝ ) |
23 |
22
|
recnd |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℂ ) |
24 |
22
|
rered |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝐴 ) = 𝐴 ) |
25 |
|
id |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
26 |
24 25
|
eqeltrd |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
27 |
|
asinsin |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
28 |
23 26 27
|
syl2anc |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
29 |
|
elpri |
⊢ ( 𝐴 ∈ { - ( π / 2 ) , ( π / 2 ) } → ( 𝐴 = - ( π / 2 ) ∨ 𝐴 = ( π / 2 ) ) ) |
30 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
31 |
|
asinneg |
⊢ ( 1 ∈ ℂ → ( arcsin ‘ - 1 ) = - ( arcsin ‘ 1 ) ) |
32 |
30 31
|
ax-mp |
⊢ ( arcsin ‘ - 1 ) = - ( arcsin ‘ 1 ) |
33 |
|
asin1 |
⊢ ( arcsin ‘ 1 ) = ( π / 2 ) |
34 |
33
|
negeqi |
⊢ - ( arcsin ‘ 1 ) = - ( π / 2 ) |
35 |
32 34
|
eqtri |
⊢ ( arcsin ‘ - 1 ) = - ( π / 2 ) |
36 |
|
fveq2 |
⊢ ( 𝐴 = - ( π / 2 ) → ( sin ‘ 𝐴 ) = ( sin ‘ - ( π / 2 ) ) ) |
37 |
3
|
recni |
⊢ ( π / 2 ) ∈ ℂ |
38 |
|
sinneg |
⊢ ( ( π / 2 ) ∈ ℂ → ( sin ‘ - ( π / 2 ) ) = - ( sin ‘ ( π / 2 ) ) ) |
39 |
37 38
|
ax-mp |
⊢ ( sin ‘ - ( π / 2 ) ) = - ( sin ‘ ( π / 2 ) ) |
40 |
|
sinhalfpi |
⊢ ( sin ‘ ( π / 2 ) ) = 1 |
41 |
40
|
negeqi |
⊢ - ( sin ‘ ( π / 2 ) ) = - 1 |
42 |
39 41
|
eqtri |
⊢ ( sin ‘ - ( π / 2 ) ) = - 1 |
43 |
36 42
|
eqtrdi |
⊢ ( 𝐴 = - ( π / 2 ) → ( sin ‘ 𝐴 ) = - 1 ) |
44 |
43
|
fveq2d |
⊢ ( 𝐴 = - ( π / 2 ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( arcsin ‘ - 1 ) ) |
45 |
|
id |
⊢ ( 𝐴 = - ( π / 2 ) → 𝐴 = - ( π / 2 ) ) |
46 |
35 44 45
|
3eqtr4a |
⊢ ( 𝐴 = - ( π / 2 ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
47 |
|
fveq2 |
⊢ ( 𝐴 = ( π / 2 ) → ( sin ‘ 𝐴 ) = ( sin ‘ ( π / 2 ) ) ) |
48 |
47 40
|
eqtrdi |
⊢ ( 𝐴 = ( π / 2 ) → ( sin ‘ 𝐴 ) = 1 ) |
49 |
48
|
fveq2d |
⊢ ( 𝐴 = ( π / 2 ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( arcsin ‘ 1 ) ) |
50 |
|
id |
⊢ ( 𝐴 = ( π / 2 ) → 𝐴 = ( π / 2 ) ) |
51 |
33 49 50
|
3eqtr4a |
⊢ ( 𝐴 = ( π / 2 ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
52 |
46 51
|
jaoi |
⊢ ( ( 𝐴 = - ( π / 2 ) ∨ 𝐴 = ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
53 |
29 52
|
syl |
⊢ ( 𝐴 ∈ { - ( π / 2 ) , ( π / 2 ) } → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
54 |
28 53
|
jaoi |
⊢ ( ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∨ 𝐴 ∈ { - ( π / 2 ) , ( π / 2 ) } ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |
55 |
21 54
|
sylbi |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |