Definition df-atan

Description: Define the arctangent function. See also remarks for df-asin . Unlike arcsin and arccos , this function is not defined everywhere, because tan ( z ) =/= +-i for all z e. CC . For all other z , there is a formula for arctan ( z ) in terms of log , and we take that as the definition. Branch points are at +- i ; branch cuts are on the pure imaginary axis not between -ui and i , which is to say { z e. CC | ( _i x. z ) e. ( -oo , -u 1 ) u. ( 1 , +oo ) } . (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	df-atan	|- arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		catan	|- arctan
1		vx	|- x
2		cc	|- CC
3		ci	|- _i
4	3	cneg	|- -u _i
5	4 3	cpr	|- { -u _i , _i }
6	2 5	cdif	|- ( CC \ { -u _i , _i } )
7		cdiv	|- /
8		c2	|- 2
9	3 8 7	co	|- ( _i / 2 )
10		cmul	|- x.
11		clog	|- log
12		c1	|- 1
13		cmin	|- -
14	1	cv	|- x
15	3 14 10	co	|- ( _i x. x )
16	12 15 13	co	|- ( 1 - ( _i x. x ) )
17	16 11	cfv	|- ( log ` ( 1 - ( _i x. x ) ) )
18		caddc	|- +
19	12 15 18	co	|- ( 1 + ( _i x. x ) )
20	19 11	cfv	|- ( log ` ( 1 + ( _i x. x ) ) )
21	17 20 13	co	|- ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) )
22	9 21 10	co	|- ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) )
23	1 6 22	cmpt	|- ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
24	0 23	wceq	|- arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )