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 ( 𝐴 ∈ ℂ → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 asincl ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) ∈ ℂ )
2 sinval ⊢ ( ( arcsin ‘ 𝐴 ) ∈ ℂ → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / ( 2 · i ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / ( 2 · i ) ) )
4 ax-icn ⊢ i ∈ ℂ
5 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
6 4 5 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
7 6 negcld ⊢ ( 𝐴 ∈ ℂ → - ( i · 𝐴 ) ∈ ℂ )
8 ax-1cn ⊢ 1 ∈ ℂ
9 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
10 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
11 8 9 10 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
12 11 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
13 6 7 12 pnpcan2d ⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) − ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) )
14 efiasin ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
15 mulneg12 ⊢ ( ( i ∈ ℂ ∧ ( arcsin ‘ 𝐴 ) ∈ ℂ ) → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
16 4 1 15 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
17 asinneg ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = - ( arcsin ‘ 𝐴 ) )
18 17 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( arcsin ‘ - 𝐴 ) ) = ( i · - ( arcsin ‘ 𝐴 ) ) )
19 16 18 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( - i · ( arcsin ‘ 𝐴 ) ) = ( i · ( arcsin ‘ - 𝐴 ) ) )
20 19 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) = ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) )
21 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
22 efiasin ⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
23 21 22 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ - 𝐴 ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
24 mulneg2 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
25 4 24 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
26 sqneg ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
27 26 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( - 𝐴 ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ 2 ) ) )
28 27 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) = ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) )
29 25 28 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) = ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
30 20 23 29 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) = ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
31 14 30 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) = ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) − ( - ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
32 6 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
33 2cn ⊢ 2 ∈ ℂ
34 mulass ⊢ ( ( 2 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 2 · i ) · 𝐴 ) = ( 2 · ( i · 𝐴 ) ) )
35 33 4 34 mp3an12 ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · i ) · 𝐴 ) = ( 2 · ( i · 𝐴 ) ) )
36 6 6 subnegd ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
37 32 35 36 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · i ) · 𝐴 ) = ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) )
38 13 31 37 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) = ( ( 2 · i ) · 𝐴 ) )
39 mulcl ⊢ ( ( i ∈ ℂ ∧ ( arcsin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ )
40 4 1 39 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ )
41 efcl ⊢ ( ( i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) ∈ ℂ )
42 40 41 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) ∈ ℂ )
43 negicn ⊢ - i ∈ ℂ
44 mulcl ⊢ ( ( - i ∈ ℂ ∧ ( arcsin ‘ 𝐴 ) ∈ ℂ ) → ( - i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ )
45 43 1 44 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ )
46 efcl ⊢ ( ( - i · ( arcsin ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ∈ ℂ )
47 45 46 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ∈ ℂ )
48 42 47 subcld ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) ∈ ℂ )
49 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
50 2mulicn ⊢ ( 2 · i ) ∈ ℂ
51 50 a1i ⊢ ( 𝐴 ∈ ℂ → ( 2 · i ) ∈ ℂ )
52 2muline0 ⊢ ( 2 · i ) ≠ 0
53 52 a1i ⊢ ( 𝐴 ∈ ℂ → ( 2 · i ) ≠ 0 )
54 48 49 51 53 divmul2d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / ( 2 · i ) ) = 𝐴 ↔ ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) = ( ( 2 · i ) · 𝐴 ) ) )
55 38 54 mpbird ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · ( arcsin ‘ 𝐴 ) ) ) − ( exp ‘ ( - i · ( arcsin ‘ 𝐴 ) ) ) ) / ( 2 · i ) ) = 𝐴 )
56 3 55 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( arcsin ‘ 𝐴 ) ) = 𝐴 )