Theorem atancl

Description: Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atancl	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		atanf	⊢ arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ
2	1	ffvelrni	⊢ ( 𝐴 ∈ ( ℂ ∖ { - i , i } ) → ( arctan ‘ 𝐴 ) ∈ ℂ )
3	1	fdmi	⊢ dom arctan = ( ℂ ∖ { - i , i } )
4	2 3	eleq2s	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) ∈ ℂ )