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

Metamath Proof Explorer

Theorem atanf

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

Ref Expression
Assertion atanf arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ

Proof

Step Hyp Ref Expression
1 df-atan ⊢ arctan = ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )
2 ovex ⊢ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) ∈ V
3 2 1 dmmpti ⊢ dom arctan = ( ℂ ∖ { - i , i } )
4 3 eleq2i ⊢ ( 𝑥 ∈ dom arctan ↔ 𝑥 ∈ ( ℂ ∖ { - i , i } ) )
5 ax-icn ⊢ i ∈ ℂ
6 halfcl ⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
7 5 6 ax-mp ⊢ ( i / 2 ) ∈ ℂ
8 ax-1cn ⊢ 1 ∈ ℂ
9 atandm2 ⊢ ( 𝑥 ∈ dom arctan ↔ ( 𝑥 ∈ ℂ ∧ ( 1 − ( i · 𝑥 ) ) ≠ 0 ∧ ( 1 + ( i · 𝑥 ) ) ≠ 0 ) )
10 9 simp1bi ⊢ ( 𝑥 ∈ dom arctan → 𝑥 ∈ ℂ )
11 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ )
12 5 10 11 sylancr ⊢ ( 𝑥 ∈ dom arctan → ( i · 𝑥 ) ∈ ℂ )
13 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝑥 ) ∈ ℂ ) → ( 1 − ( i · 𝑥 ) ) ∈ ℂ )
14 8 12 13 sylancr ⊢ ( 𝑥 ∈ dom arctan → ( 1 − ( i · 𝑥 ) ) ∈ ℂ )
15 9 simp2bi ⊢ ( 𝑥 ∈ dom arctan → ( 1 − ( i · 𝑥 ) ) ≠ 0 )
16 14 15 logcld ⊢ ( 𝑥 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝑥 ) ) ) ∈ ℂ )
17 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝑥 ) ∈ ℂ ) → ( 1 + ( i · 𝑥 ) ) ∈ ℂ )
18 8 12 17 sylancr ⊢ ( 𝑥 ∈ dom arctan → ( 1 + ( i · 𝑥 ) ) ∈ ℂ )
19 9 simp3bi ⊢ ( 𝑥 ∈ dom arctan → ( 1 + ( i · 𝑥 ) ) ≠ 0 )
20 18 19 logcld ⊢ ( 𝑥 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ∈ ℂ )
21 16 20 subcld ⊢ ( 𝑥 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ∈ ℂ )
22 mulcl ⊢ ( ( ( i / 2 ) ∈ ℂ ∧ ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ∈ ℂ ) → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) ∈ ℂ )
23 7 21 22 sylancr ⊢ ( 𝑥 ∈ dom arctan → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) ∈ ℂ )
24 4 23 sylbir ⊢ ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) ∈ ℂ )
25 1 24 fmpti ⊢ arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ