Theorem atanf

Description: Domain and range 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 } ) ⟶ ℂ