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\in ℂ\to \sin arcsin\left(A\right)=A$$

Proof

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