Metamath Proof Explorer

Theorem efiasin

Description: The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion efiasin 
|- ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 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 oveq2d 
 |-  ( A e. CC -> ( _i x. ( arcsin ` A ) ) = ( _i x. ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( A e. CC -> _i e. CC )
5 negicn 
 |-  -u _i e. CC
6 5 a1i 
 |-  ( A e. CC -> -u _i e. CC )
7 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
8 3 7 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
9 ax-1cn 
 |-  1 e. CC
10 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
11 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
12 9 10 11 sylancr 
 |-  ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
13 12 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
14 8 13 addcld 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC )
15 asinlem 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 )
16 14 15 logcld 
 |-  ( A e. CC -> ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC )
17 4 6 16 mulassd 
 |-  ( A e. CC -> ( ( _i x. -u _i ) x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( _i x. ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
18 3 3 mulneg2i 
 |-  ( _i x. -u _i ) = -u ( _i x. _i )
19 ixi 
 |-  ( _i x. _i ) = -u 1
20 19 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
21 negneg1e1 
 |-  -u -u 1 = 1
22 18 20 21 3eqtri 
 |-  ( _i x. -u _i ) = 1
23 22 oveq1i 
 |-  ( ( _i x. -u _i ) x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( 1 x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
24 16 mulid2d 
 |-  ( A e. CC -> ( 1 x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
25 23 24 syl5eq 
 |-  ( A e. CC -> ( ( _i x. -u _i ) x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
26 2 17 25 3eqtr2d 
 |-  ( A e. CC -> ( _i x. ( arcsin ` A ) ) = ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
27 26 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
28 eflog 
 |-  ( ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 ) -> ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
29 14 15 28 syl2anc 
 |-  ( A e. CC -> ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
30 27 29 eqtrd 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )