Metamath Proof Explorer

Theorem acoscos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acoscos 
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` A ) ) = A )

Proof

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 )