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 ‘ 𝐴 ) ) = 𝐴 )