This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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