Metamath Proof Explorer

Theorem asinval

Description: Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion asinval 
|- ( A e. CC -> ( arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = A -> ( _i x. x ) = ( _i x. A ) )
2 oveq1 
 |-  ( x = A -> ( x ^ 2 ) = ( A ^ 2 ) )
3 2 oveq2d 
 |-  ( x = A -> ( 1 - ( x ^ 2 ) ) = ( 1 - ( A ^ 2 ) ) )
4 3 fveq2d 
 |-  ( x = A -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )
5 1 4 oveq12d 
 |-  ( x = A -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
6 5 fveq2d 
 |-  ( x = A -> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
7 6 oveq2d 
 |-  ( x = A -> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
8 df-asin 
 |-  arcsin = ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
9 ovex 
 |-  ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( A e. CC -> ( arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )