Metamath Proof Explorer

Theorem asinbnd

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

Ref Expression
Assertion asinbnd 
|- ( A e. CC -> ( Re ` ( arcsin ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 asinval 
 |-  ( A e. CC -> ( arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
2 1 fveq2d 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) = ( Re ` ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
3 ax-icn 
 |-  _i e. CC
4 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
5 3 4 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
6 ax-1cn 
 |-  1 e. CC
7 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
8 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
9 6 7 8 sylancr 
 |-  ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
10 9 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
11 5 10 addcld 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC )
12 asinlem 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 )
13 11 12 logcld 
 |-  ( A e. CC -> ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC )
14 imre 
 |-  ( ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( Re ` ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
15 13 14 syl 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( Re ` ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
16 2 15 eqtr4d 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) = ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
17 asinlem3 
 |-  ( A e. CC -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
18 argrege0 
 |-  ( ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 /\ 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
19 11 12 17 18 syl3anc 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
20 16 19 eqeltrd 
 |-  ( A e. CC -> ( Re ` ( arcsin ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )