Theorem asinf

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

	Ref	Expression
Assertion	asinf	$$⊢arcsin:ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-asin	$$⊢arcsin=\left(x\in ℂ⟼\left(-\mathrm{i}\right)\log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\right)$$
2		negicn	$$⊢-\mathrm{i}\in ℂ$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge x\in ℂ\right)\to \mathrm{i}x\in ℂ$$
5	3 4	mpan	$$⊢x\in ℂ\to \mathrm{i}x\in ℂ$$
6		ax-1cn	$$⊢1\in ℂ$$
7		sqcl	$$⊢x\in ℂ\to x^2\in ℂ$$
8		subcl	$$⊢\left(1\in ℂ\wedge x^2\in ℂ\right)\to 1-x^2\in ℂ$$
9	6 7 8	sylancr	$$⊢x\in ℂ\to 1-x^2\in ℂ$$
10	9	sqrtcld	$$⊢x\in ℂ\to \sqrt{1-x^2}\in ℂ$$
11	5 10	addcld	$$⊢x\in ℂ\to \mathrm{i}x+\sqrt{1-x^2}\in ℂ$$
12		asinlem	$$⊢x\in ℂ\to \mathrm{i}x+\sqrt{1-x^2}\ne 0$$
13	11 12	logcld	$$⊢x\in ℂ\to \log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\in ℂ$$
14		mulcl	$$⊢\left(-\mathrm{i}\in ℂ\wedge \log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\in ℂ\right)\to \left(-\mathrm{i}\right)\log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\in ℂ$$
15	2 13 14	sylancr	$$⊢x\in ℂ\to \left(-\mathrm{i}\right)\log \left(\mathrm{i}x+\sqrt{1-x^2}\right)\in ℂ$$
16	1 15	fmpti	$$⊢arcsin:ℂ⟶ℂ$$