Theorem asinval

Description: Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2		oveq1	$$⊢x=A\to x^2=A^2$$
3	2	oveq2d	$$⊢x=A\to 1-x^2=1-A^2$$
4	3	fveq2d	$$⊢x=A\to \sqrt{1-x^2}=\sqrt{1-A^2}$$
5	1 4	oveq12d	$$⊢x=A\to \mathrm{i}x+\sqrt{1-x^2}=\mathrm{i}A+\sqrt{1-A^2}$$
6	5	fveq2d	$$⊢x=A\to \log \left(\mathrm{i}x+\sqrt{1-x^2}\right)=\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
7	6	oveq2d	$$⊢x=A\to \left(-\mathrm{i}\right)\log \left(\mathrm{i}x+\sqrt{1-x^2}\right)=\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$
8		df-asin	$$⊢arcsin=\left(x\in ℂ⟼\left(-\mathrm{i}\right)\log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\right)$$
9		ovex	$$⊢\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢A\in ℂ\to arcsin\left(A\right)=\left(-\mathrm{i}\right)\log \left(\mathrm{i}A+\sqrt{1-A^2}\right)$$