Theorem efiasin

Description: The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	efiasin	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}=\mathrm{i}A+\sqrt{1-A^2}$$

Proof

Step	Hyp	Ref	Expression
1		asinval	$$⊢A\in ℂ\to arcsin\left(A\right)=\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
2	1	oveq2d	$$⊢A\in ℂ\to \mathrm{i}arcsin\left(A\right)=\mathrm{i}\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4	3	a1i	$$⊢A\in ℂ\to \mathrm{i}\in ℂ$$
5		negicn	$$⊢-\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢A\in ℂ\to -\mathrm{i}\in ℂ$$
7		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
8	3 7	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
9		ax-1cn	$$⊢1\in ℂ$$
10		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
11		subcl	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\to 1-A^2\in ℂ$$
12	9 10 11	sylancr	$$⊢A\in ℂ\to 1-A^2\in ℂ$$
13	12	sqrtcld	$$⊢A\in ℂ\to \sqrt{1-A^2}\in ℂ$$
14	8 13	addcld	$$⊢A\in ℂ\to \mathrm{i}A+\sqrt{1-A^2}\in ℂ$$
15		asinlem	$$⊢A\in ℂ\to \mathrm{i}A+\sqrt{1-A^2}\ne 0$$
16	14 15	logcld	$$⊢A\in ℂ\to \log \left(\mathrm{i}A+\sqrt{1-A^2}\right)\in ℂ$$
17	4 6 16	mulassd	$$⊢A\in ℂ\to \mathrm{i}\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)=\mathrm{i}\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
18	3 3	mulneg2i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=-\mathrm{i}\mathrm{i}$$
19		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
20	19	negeqi	$$⊢-\mathrm{i}\mathrm{i}=--1$$
21		negneg1e1	$$⊢--1=1$$
22	18 20 21	3eqtri	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=1$$
23	22	oveq1i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)=1\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
24	16	mulid2d	$$⊢A\in ℂ\to 1\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)=\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
25	23 24	syl5eq	$$⊢A\in ℂ\to \mathrm{i}\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)=\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
26	2 17 25	3eqtr2d	$$⊢A\in ℂ\to \mathrm{i}arcsin\left(A\right)=\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
27	26	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}={\mathrm{e}}^{\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)}$$
28		eflog	$$⊢\left(\mathrm{i}A+\sqrt{1-A^2}\in ℂ\wedge \mathrm{i}A+\sqrt{1-A^2}\ne 0\right)\to {\mathrm{e}}^{\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)}=\mathrm{i}A+\sqrt{1-A^2}$$
29	14 15 28	syl2anc	$$⊢A\in ℂ\to {\mathrm{e}}^{\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)}=\mathrm{i}A+\sqrt{1-A^2}$$
30	27 29	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}arcsin\left(A\right)}=\mathrm{i}A+\sqrt{1-A^2}$$