Metamath Proof Explorer

Theorem sinasin

Description: The arcsine function is an inverse to sin . This is the main property that justifies the notation arcsin or sin ^ -u 1 . Because sin is not an injection, the other converse identity asinsin is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion sinasin 
|- ( A e. CC -> ( sin ` ( arcsin ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
2 sinval 
 |-  ( ( arcsin ` A ) e. CC -> ( sin ` ( arcsin ` A ) ) = ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / ( 2 x. _i ) ) )
3 1 2 syl 
 |-  ( A e. CC -> ( sin ` ( arcsin ` A ) ) = ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / ( 2 x. _i ) ) )
4 ax-icn 
 |-  _i e. CC
5 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
6 4 5 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
7 6 negcld 
 |-  ( A e. CC -> -u ( _i x. A ) e. CC )
8 ax-1cn 
 |-  1 e. CC
9 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
10 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
11 8 9 10 sylancr 
 |-  ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
12 11 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
13 6 7 12 pnpcan2d 
 |-  ( A e. CC -> ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) - ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( ( _i x. A ) - -u ( _i x. A ) ) )
14 efiasin 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
15 mulneg12 
 |-  ( ( _i e. CC /\ ( arcsin ` A ) e. CC ) -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. -u ( arcsin ` A ) ) )
16 4 1 15 sylancr 
 |-  ( A e. CC -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. -u ( arcsin ` A ) ) )
17 asinneg 
 |-  ( A e. CC -> ( arcsin ` -u A ) = -u ( arcsin ` A ) )
18 17 oveq2d 
 |-  ( A e. CC -> ( _i x. ( arcsin ` -u A ) ) = ( _i x. -u ( arcsin ` A ) ) )
19 16 18 eqtr4d 
 |-  ( A e. CC -> ( -u _i x. ( arcsin ` A ) ) = ( _i x. ( arcsin ` -u A ) ) )
20 19 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) = ( exp ` ( _i x. ( arcsin ` -u A ) ) ) )
21 negcl 
 |-  ( A e. CC -> -u A e. CC )
22 efiasin 
 |-  ( -u A e. CC -> ( exp ` ( _i x. ( arcsin ` -u A ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
23 21 22 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` -u A ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
24 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
25 4 24 mpan 
 |-  ( A e. CC -> ( _i x. -u A ) = -u ( _i x. A ) )
26 sqneg 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
27 26 oveq2d 
 |-  ( A e. CC -> ( 1 - ( -u A ^ 2 ) ) = ( 1 - ( A ^ 2 ) ) )
28 27 fveq2d 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) = ( sqrt ` ( 1 - ( A ^ 2 ) ) ) )
29 25 28 oveq12d 
 |-  ( A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) = ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
30 20 23 29 3eqtrd 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) = ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
31 14 30 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) = ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) - ( -u ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
32 6 2timesd 
 |-  ( A e. CC -> ( 2 x. ( _i x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
33 2cn 
 |-  2 e. CC
34 mulass 
 |-  ( ( 2 e. CC /\ _i e. CC /\ A e. CC ) -> ( ( 2 x. _i ) x. A ) = ( 2 x. ( _i x. A ) ) )
35 33 4 34 mp3an12 
 |-  ( A e. CC -> ( ( 2 x. _i ) x. A ) = ( 2 x. ( _i x. A ) ) )
36 6 6 subnegd 
 |-  ( A e. CC -> ( ( _i x. A ) - -u ( _i x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
37 32 35 36 3eqtr4d 
 |-  ( A e. CC -> ( ( 2 x. _i ) x. A ) = ( ( _i x. A ) - -u ( _i x. A ) ) )
38 13 31 37 3eqtr4d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) = ( ( 2 x. _i ) x. A ) )
39 mulcl 
 |-  ( ( _i e. CC /\ ( arcsin ` A ) e. CC ) -> ( _i x. ( arcsin ` A ) ) e. CC )
40 4 1 39 sylancr 
 |-  ( A e. CC -> ( _i x. ( arcsin ` A ) ) e. CC )
41 efcl 
 |-  ( ( _i x. ( arcsin ` A ) ) e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) e. CC )
42 40 41 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. ( arcsin ` A ) ) ) e. CC )
43 negicn 
 |-  -u _i e. CC
44 mulcl 
 |-  ( ( -u _i e. CC /\ ( arcsin ` A ) e. CC ) -> ( -u _i x. ( arcsin ` A ) ) e. CC )
45 43 1 44 sylancr 
 |-  ( A e. CC -> ( -u _i x. ( arcsin ` A ) ) e. CC )
46 efcl 
 |-  ( ( -u _i x. ( arcsin ` A ) ) e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) e. CC )
47 45 46 syl 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( arcsin ` A ) ) ) e. CC )
48 42 47 subcld 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) e. CC )
49 id 
 |-  ( A e. CC -> A e. CC )
50 2mulicn 
 |-  ( 2 x. _i ) e. CC
51 50 a1i 
 |-  ( A e. CC -> ( 2 x. _i ) e. CC )
52 2muline0 
 |-  ( 2 x. _i ) =/= 0
53 52 a1i 
 |-  ( A e. CC -> ( 2 x. _i ) =/= 0 )
54 48 49 51 53 divmul2d 
 |-  ( A e. CC -> ( ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / ( 2 x. _i ) ) = A <-> ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) = ( ( 2 x. _i ) x. A ) ) )
55 38 54 mpbird 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. ( arcsin ` A ) ) ) - ( exp ` ( -u _i x. ( arcsin ` A ) ) ) ) / ( 2 x. _i ) ) = A )
56 3 55 eqtrd 
 |-  ( A e. CC -> ( sin ` ( arcsin ` A ) ) = A )