This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 : ℂ ⟶ ℂ