Metamath Proof Explorer


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 i i i 2 log 1 i x log 1 + i x

Detailed syntax breakdown

Step Hyp Ref Expression
0 catan class arctan
1 vx setvar x
2 cc class
3 ci class i
4 3 cneg class i
5 4 3 cpr class i i
6 2 5 cdif class i i
7 cdiv class ÷
8 c2 class 2
9 3 8 7 co class i 2
10 cmul class ×
11 clog class log
12 c1 class 1
13 cmin class
14 1 cv setvar x
15 3 14 10 co class i x
16 12 15 13 co class 1 i x
17 16 11 cfv class log 1 i x
18 caddc class +
19 12 15 18 co class 1 + i x
20 19 11 cfv class log 1 + i x
21 17 20 13 co class log 1 i x log 1 + i x
22 9 21 10 co class i 2 log 1 i x log 1 + i x
23 1 6 22 cmpt class x i i i 2 log 1 i x log 1 + i x
24 0 23 wceq wff arctan = x i i i 2 log 1 i x log 1 + i x