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 )