Step |
Hyp |
Ref |
Expression |
1 |
|
coscl |
|- ( A e. CC -> ( cos ` A ) e. CC ) |
2 |
1
|
adantr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( cos ` A ) e. CC ) |
3 |
|
acosval |
|- ( ( cos ` A ) e. CC -> ( arccos ` ( cos ` A ) ) = ( ( _pi / 2 ) - ( arcsin ` ( cos ` A ) ) ) ) |
4 |
2 3
|
syl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` A ) ) = ( ( _pi / 2 ) - ( arcsin ` ( cos ` A ) ) ) ) |
5 |
|
picn |
|- _pi e. CC |
6 |
|
halfcl |
|- ( _pi e. CC -> ( _pi / 2 ) e. CC ) |
7 |
5 6
|
ax-mp |
|- ( _pi / 2 ) e. CC |
8 |
|
simpl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> A e. CC ) |
9 |
|
nncan |
|- ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( ( _pi / 2 ) - ( ( _pi / 2 ) - A ) ) = A ) |
10 |
7 8 9
|
sylancr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - ( ( _pi / 2 ) - A ) ) = A ) |
11 |
10
|
fveq2d |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( cos ` ( ( _pi / 2 ) - ( ( _pi / 2 ) - A ) ) ) = ( cos ` A ) ) |
12 |
|
subcl |
|- ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( ( _pi / 2 ) - A ) e. CC ) |
13 |
7 8 12
|
sylancr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - A ) e. CC ) |
14 |
|
coshalfpim |
|- ( ( ( _pi / 2 ) - A ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( ( _pi / 2 ) - A ) ) ) = ( sin ` ( ( _pi / 2 ) - A ) ) ) |
15 |
13 14
|
syl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( cos ` ( ( _pi / 2 ) - ( ( _pi / 2 ) - A ) ) ) = ( sin ` ( ( _pi / 2 ) - A ) ) ) |
16 |
11 15
|
eqtr3d |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( cos ` A ) = ( sin ` ( ( _pi / 2 ) - A ) ) ) |
17 |
16
|
fveq2d |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arcsin ` ( cos ` A ) ) = ( arcsin ` ( sin ` ( ( _pi / 2 ) - A ) ) ) ) |
18 |
|
halfpire |
|- ( _pi / 2 ) e. RR |
19 |
18
|
recni |
|- ( _pi / 2 ) e. CC |
20 |
|
resub |
|- ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( Re ` ( ( _pi / 2 ) - A ) ) = ( ( Re ` ( _pi / 2 ) ) - ( Re ` A ) ) ) |
21 |
19 8 20
|
sylancr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` ( ( _pi / 2 ) - A ) ) = ( ( Re ` ( _pi / 2 ) ) - ( Re ` A ) ) ) |
22 |
|
rere |
|- ( ( _pi / 2 ) e. RR -> ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) ) |
23 |
18 22
|
ax-mp |
|- ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) |
24 |
23
|
oveq1i |
|- ( ( Re ` ( _pi / 2 ) ) - ( Re ` A ) ) = ( ( _pi / 2 ) - ( Re ` A ) ) |
25 |
21 24
|
eqtrdi |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` ( ( _pi / 2 ) - A ) ) = ( ( _pi / 2 ) - ( Re ` A ) ) ) |
26 |
|
recl |
|- ( A e. CC -> ( Re ` A ) e. RR ) |
27 |
26
|
adantr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` A ) e. RR ) |
28 |
|
resubcl |
|- ( ( ( _pi / 2 ) e. RR /\ ( Re ` A ) e. RR ) -> ( ( _pi / 2 ) - ( Re ` A ) ) e. RR ) |
29 |
18 27 28
|
sylancr |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - ( Re ` A ) ) e. RR ) |
30 |
18
|
a1i |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( _pi / 2 ) e. RR ) |
31 |
|
neghalfpire |
|- -u ( _pi / 2 ) e. RR |
32 |
31
|
a1i |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> -u ( _pi / 2 ) e. RR ) |
33 |
|
eliooord |
|- ( ( Re ` A ) e. ( 0 (,) _pi ) -> ( 0 < ( Re ` A ) /\ ( Re ` A ) < _pi ) ) |
34 |
33
|
adantl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( 0 < ( Re ` A ) /\ ( Re ` A ) < _pi ) ) |
35 |
34
|
simprd |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` A ) < _pi ) |
36 |
19 19
|
subnegi |
|- ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = ( ( _pi / 2 ) + ( _pi / 2 ) ) |
37 |
|
pidiv2halves |
|- ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi |
38 |
36 37
|
eqtri |
|- ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi |
39 |
35 38
|
breqtrrdi |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` A ) < ( ( _pi / 2 ) - -u ( _pi / 2 ) ) ) |
40 |
27 30 32 39
|
ltsub13d |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> -u ( _pi / 2 ) < ( ( _pi / 2 ) - ( Re ` A ) ) ) |
41 |
34
|
simpld |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> 0 < ( Re ` A ) ) |
42 |
|
ltsubpos |
|- ( ( ( Re ` A ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( 0 < ( Re ` A ) <-> ( ( _pi / 2 ) - ( Re ` A ) ) < ( _pi / 2 ) ) ) |
43 |
27 18 42
|
sylancl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( 0 < ( Re ` A ) <-> ( ( _pi / 2 ) - ( Re ` A ) ) < ( _pi / 2 ) ) ) |
44 |
41 43
|
mpbid |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - ( Re ` A ) ) < ( _pi / 2 ) ) |
45 |
31
|
rexri |
|- -u ( _pi / 2 ) e. RR* |
46 |
18
|
rexri |
|- ( _pi / 2 ) e. RR* |
47 |
|
elioo2 |
|- ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( ( _pi / 2 ) - ( Re ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( ( _pi / 2 ) - ( Re ` A ) ) e. RR /\ -u ( _pi / 2 ) < ( ( _pi / 2 ) - ( Re ` A ) ) /\ ( ( _pi / 2 ) - ( Re ` A ) ) < ( _pi / 2 ) ) ) ) |
48 |
45 46 47
|
mp2an |
|- ( ( ( _pi / 2 ) - ( Re ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( ( _pi / 2 ) - ( Re ` A ) ) e. RR /\ -u ( _pi / 2 ) < ( ( _pi / 2 ) - ( Re ` A ) ) /\ ( ( _pi / 2 ) - ( Re ` A ) ) < ( _pi / 2 ) ) ) |
49 |
29 40 44 48
|
syl3anbrc |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - ( Re ` A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) |
50 |
25 49
|
eqeltrd |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( Re ` ( ( _pi / 2 ) - A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) |
51 |
|
asinsin |
|- ( ( ( ( _pi / 2 ) - A ) e. CC /\ ( Re ` ( ( _pi / 2 ) - A ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` ( ( _pi / 2 ) - A ) ) ) = ( ( _pi / 2 ) - A ) ) |
52 |
13 50 51
|
syl2anc |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arcsin ` ( sin ` ( ( _pi / 2 ) - A ) ) ) = ( ( _pi / 2 ) - A ) ) |
53 |
17 52
|
eqtr2d |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - A ) = ( arcsin ` ( cos ` A ) ) ) |
54 |
|
asincl |
|- ( ( cos ` A ) e. CC -> ( arcsin ` ( cos ` A ) ) e. CC ) |
55 |
2 54
|
syl |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arcsin ` ( cos ` A ) ) e. CC ) |
56 |
|
subsub23 |
|- ( ( ( _pi / 2 ) e. CC /\ A e. CC /\ ( arcsin ` ( cos ` A ) ) e. CC ) -> ( ( ( _pi / 2 ) - A ) = ( arcsin ` ( cos ` A ) ) <-> ( ( _pi / 2 ) - ( arcsin ` ( cos ` A ) ) ) = A ) ) |
57 |
19 8 55 56
|
mp3an2i |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( ( _pi / 2 ) - A ) = ( arcsin ` ( cos ` A ) ) <-> ( ( _pi / 2 ) - ( arcsin ` ( cos ` A ) ) ) = A ) ) |
58 |
53 57
|
mpbid |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( ( _pi / 2 ) - ( arcsin ` ( cos ` A ) ) ) = A ) |
59 |
4 58
|
eqtrd |
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` A ) ) = A ) |