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 )