Theorem atanf

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

	Ref	Expression
Assertion	atanf	|- arctan : ( CC \ { -u _i , _i } ) --> CC

Proof

Step	Hyp	Ref	Expression
1		df-atan	|- arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
2		ovex	|- ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. _V
3	2 1	dmmpti	|- dom arctan = ( CC \ { -u _i , _i } )
4	3	eleq2i	|- ( x e. dom arctan <-> x e. ( CC \ { -u _i , _i } ) )
5		ax-icn	|- _i e. CC
6		halfcl	|- ( _i e. CC -> ( _i / 2 ) e. CC )
7	5 6	ax-mp	|- ( _i / 2 ) e. CC
8		ax-1cn	|- 1 e. CC
9		atandm2	|- ( x e. dom arctan <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
10	9	simp1bi	|- ( x e. dom arctan -> x e. CC )
11		mulcl	|- ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
12	5 10 11	sylancr	|- ( x e. dom arctan -> ( _i x. x ) e. CC )
13		subcl	|- ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
14	8 12 13	sylancr	|- ( x e. dom arctan -> ( 1 - ( _i x. x ) ) e. CC )
15	9	simp2bi	|- ( x e. dom arctan -> ( 1 - ( _i x. x ) ) =/= 0 )
16	14 15	logcld	|- ( x e. dom arctan -> ( log ` ( 1 - ( _i x. x ) ) ) e. CC )
17		addcl	|- ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
18	8 12 17	sylancr	|- ( x e. dom arctan -> ( 1 + ( _i x. x ) ) e. CC )
19	9	simp3bi	|- ( x e. dom arctan -> ( 1 + ( _i x. x ) ) =/= 0 )
20	18 19	logcld	|- ( x e. dom arctan -> ( log ` ( 1 + ( _i x. x ) ) ) e. CC )
21	16 20	subcld	|- ( x e. dom arctan -> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC )
22		mulcl	|- ( ( ( _i / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC ) -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
23	7 21 22	sylancr	|- ( x e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
24	4 23	sylbir	|- ( x e. ( CC \ { -u _i , _i } ) -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
25	1 24	fmpti	|- arctan : ( CC \ { -u _i , _i } ) --> CC