Metamath Proof Explorer

Theorem asinf

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

Ref Expression
Assertion asinf 
|- arcsin : CC --> CC

Proof

Step Hyp Ref Expression
1 df-asin 
 |-  arcsin = ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
2 negicn 
 |-  -u _i e. CC
3 ax-icn 
 |-  _i e. CC
4 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
5 3 4 mpan 
 |-  ( x e. CC -> ( _i x. x ) e. CC )
6 ax-1cn 
 |-  1 e. CC
7 sqcl 
 |-  ( x e. CC -> ( x ^ 2 ) e. CC )
8 subcl 
 |-  ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 - ( x ^ 2 ) ) e. CC )
9 6 7 8 sylancr 
 |-  ( x e. CC -> ( 1 - ( x ^ 2 ) ) e. CC )
10 9 sqrtcld 
 |-  ( x e. CC -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC )
11 5 10 addcld 
 |-  ( x e. CC -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
12 asinlem 
 |-  ( x e. CC -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
13 11 12 logcld 
 |-  ( x e. CC -> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
14 mulcl 
 |-  ( ( -u _i e. CC /\ ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC ) -> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) e. CC )
15 2 13 14 sylancr 
 |-  ( x e. CC -> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) e. CC )
16 1 15 fmpti 
 |-  arcsin : CC --> CC