Theorem atancl

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

	Ref	Expression
Assertion	atancl	|- ( A e. dom arctan -> ( arctan ` A ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		atanf	|- arctan : ( CC \ { -u _i , _i } ) --> CC
2	1	ffvelcdmi	|- ( A e. ( CC \ { -u _i , _i } ) -> ( arctan ` A ) e. CC )
3	1	fdmi	|- dom arctan = ( CC \ { -u _i , _i } )
4	2 3	eleq2s	|- ( A e. dom arctan -> ( arctan ` A ) e. CC )