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 ) ) ) ) ) )

Metamath Proof Explorer

Definition df-atan

Detailed syntax breakdown