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 = ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) )
2		negicn	⊢ - i ∈ ℂ
3		ax-icn	⊢ i ∈ ℂ
4		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ )
5	3 4	mpan	⊢ ( 𝑥 ∈ ℂ → ( i · 𝑥 ) ∈ ℂ )
6		ax-1cn	⊢ 1 ∈ ℂ
7		sqcl	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
8		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
9	6 7 8	sylancr	⊢ ( 𝑥 ∈ ℂ → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
10	9	sqrtcld	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ )
11	5 10	addcld	⊢ ( 𝑥 ∈ ℂ → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ )
12		asinlem	⊢ ( 𝑥 ∈ ℂ → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 )
13	11 12	logcld	⊢ ( 𝑥 ∈ ℂ → ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ )
14		mulcl	⊢ ( ( - i ∈ ℂ ∧ ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) → ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ∈ ℂ )
15	2 13 14	sylancr	⊢ ( 𝑥 ∈ ℂ → ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ∈ ℂ )
16	1 15	fmpti	⊢ arcsin : ℂ ⟶ ℂ