Metamath Proof Explorer

Theorem acosbnd

Description: The arccosine function has range within a vertical strip of the complex plane with real part between 0 and _pi . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acosbnd 
|- ( A e. CC -> ( Re ` ( arccos ` A ) ) e. ( 0 [,] _pi ) )

Proof

Step Hyp Ref Expression
1 acosval 
 |-  ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )
2 1 fveq2d 
 |-  ( A e. CC -> ( Re ` ( arccos ` A ) ) = ( Re ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) )
3 halfpire 
 |-  ( _pi / 2 ) e. RR
4 3 recni 
 |-  ( _pi / 2 ) e. CC
5 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
6 resub 
 |-  ( ( ( _pi / 2 ) e. CC /\ ( arcsin ` A ) e. CC ) -> ( Re ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( ( Re ` ( _pi / 2 ) ) - ( Re ` ( arcsin ` A ) ) ) )
7 4 5 6 sylancr 
 |-  ( A e. CC -> ( Re ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( ( Re ` ( _pi / 2 ) ) - ( Re ` ( arcsin ` A ) ) ) )
8 rere 
 |-  ( ( _pi / 2 ) e. RR -> ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) )
9 3 8 ax-mp 
 |-  ( Re ` ( _pi / 2 ) ) = ( _pi / 2 )
10 9 oveq1i 
 |-  ( ( Re ` ( _pi / 2 ) ) - ( Re ` ( arcsin ` A ) ) ) = ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) )
11 7 10 eqtrdi 
 |-  ( A e. CC -> ( Re ` ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) )
12 2 11 eqtrd 
 |-  ( A e. CC -> ( Re ` ( arccos ` A ) ) = ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) )
13 5 recld 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) e. RR )
14 resubcl 
 |-  ( ( ( _pi / 2 ) e. RR /\ ( Re ` ( arcsin ` A ) ) e. RR ) -> ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) e. RR )
15 3 13 14 sylancr 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) e. RR )
16 asinbnd 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
17 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
18 17 3 elicc2i 
 |-  ( ( Re ` ( arcsin ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( ( Re ` ( arcsin ` A ) ) e. RR /\ -u ( _pi / 2 ) <_ ( Re ` ( arcsin ` A ) ) /\ ( Re ` ( arcsin ` A ) ) <_ ( _pi / 2 ) ) )
19 16 18 sylib 
 |-  ( A e. CC -> ( ( Re ` ( arcsin ` A ) ) e. RR /\ -u ( _pi / 2 ) <_ ( Re ` ( arcsin ` A ) ) /\ ( Re ` ( arcsin ` A ) ) <_ ( _pi / 2 ) ) )
20 19 simp3d 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) <_ ( _pi / 2 ) )
21 subge0 
 |-  ( ( ( _pi / 2 ) e. RR /\ ( Re ` ( arcsin ` A ) ) e. RR ) -> ( 0 <_ ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) <-> ( Re ` ( arcsin ` A ) ) <_ ( _pi / 2 ) ) )
22 3 13 21 sylancr 
 |-  ( A e. CC -> ( 0 <_ ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) <-> ( Re ` ( arcsin ` A ) ) <_ ( _pi / 2 ) ) )
23 20 22 mpbird 
 |-  ( A e. CC -> 0 <_ ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) )
24 3 a1i 
 |-  ( A e. CC -> ( _pi / 2 ) e. RR )
25 pire 
 |-  _pi e. RR
26 25 a1i 
 |-  ( A e. CC -> _pi e. RR )
27 25 recni 
 |-  _pi e. CC
28 17 recni 
 |-  -u ( _pi / 2 ) e. CC
29 27 4 negsubi 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi - ( _pi / 2 ) )
30 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
31 27 4 4 30 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
32 29 31 eqtri 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi / 2 )
33 4 27 28 32 subaddrii 
 |-  ( ( _pi / 2 ) - _pi ) = -u ( _pi / 2 )
34 19 simp2d 
 |-  ( A e. CC -> -u ( _pi / 2 ) <_ ( Re ` ( arcsin ` A ) ) )
35 33 34 eqbrtrid 
 |-  ( A e. CC -> ( ( _pi / 2 ) - _pi ) <_ ( Re ` ( arcsin ` A ) ) )
36 24 26 13 35 subled 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) <_ _pi )
37 0re 
 |-  0 e. RR
38 37 25 elicc2i 
 |-  ( ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) e. ( 0 [,] _pi ) <-> ( ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) e. RR /\ 0 <_ ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) /\ ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) <_ _pi ) )
39 15 23 36 38 syl3anbrc 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( Re ` ( arcsin ` A ) ) ) e. ( 0 [,] _pi ) )
40 12 39 eqeltrd 
 |-  ( A e. CC -> ( Re ` ( arccos ` A ) ) e. ( 0 [,] _pi ) )