Theorem cosasin

Description: The cosine of the arcsine of A is sqrt ( 1 - A ^ 2 ) . (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	cosasin	$$⊢A\in ℂ\to \cos arcsin\left(A\right)=\sqrt{1-A^2}$$

Proof

Step	Hyp	Ref	Expression
1		asincl	$$⊢A\in ℂ\to arcsin\left(A\right)\in ℂ$$
2		cosval	$$⊢arcsin\left(A\right)\in ℂ\to \cos arcsin\left(A\right)=\frac{{\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}}{2}$$
3	1 2	syl	$$⊢A\in ℂ\to \cos arcsin\left(A\right)=\frac{{\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}}{2}$$
4		ax-1cn	$$⊢1\in ℂ$$
5		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
6		subcl	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\to 1-A^2\in ℂ$$
7	4 5 6	sylancr	$$⊢A\in ℂ\to 1-A^2\in ℂ$$
8	7	sqrtcld	$$⊢A\in ℂ\to \sqrt{1-A^2}\in ℂ$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
11	9 10	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
12	8 11 8	ppncand	$$⊢A\in ℂ\to \sqrt{1-A^2}+\mathrm{i}A+\left(\sqrt{1-A^2}-\mathrm{i}A\right)=\sqrt{1-A^2}+\sqrt{1-A^2}$$
13		efiasin	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}=\mathrm{i}A+\sqrt{1-A^2}$$
14	11 8 13	comraddd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}=\sqrt{1-A^2}+\mathrm{i}A$$
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	9 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	9 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	11	negcld	$$⊢A\in ℂ\to -\mathrm{i}A\in ℂ$$
32	31 8	addcomd	$$⊢A\in ℂ\to -\mathrm{i}A+\sqrt{1-A^2}=\sqrt{1-A^2}+\left(-\mathrm{i}A\right)$$
33	8 11	negsubd	$$⊢A\in ℂ\to \sqrt{1-A^2}+\left(-\mathrm{i}A\right)=\sqrt{1-A^2}-\mathrm{i}A$$
34	30 32 33	3eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}=\sqrt{1-A^2}-\mathrm{i}A$$
35	14 34	oveq12d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}=\sqrt{1-A^2}+\mathrm{i}A+\left(\sqrt{1-A^2}-\mathrm{i}A\right)$$
36	8	2timesd	$$⊢A\in ℂ\to 2\sqrt{1-A^2}=\sqrt{1-A^2}+\sqrt{1-A^2}$$
37	12 35 36	3eqtr4d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}=2\sqrt{1-A^2}$$
38	37	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arcsin\left(A\right)}}{2}=\frac{2\sqrt{1-A^2}}{2}$$
39		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
40		2ne0	$$⊢2\ne 0$$
41	40	a1i	$$⊢A\in ℂ\to 2\ne 0$$
42	8 39 41	divcan3d	$$⊢A\in ℂ\to \frac{2\sqrt{1-A^2}}{2}=\sqrt{1-A^2}$$
43	3 38 42	3eqtrd	$$⊢A\in ℂ\to \cos arcsin\left(A\right)=\sqrt{1-A^2}$$