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 \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{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 \div$
8		c2	$class 2$
9	3 8 7	co	$class (\frac{i}{2})$
10		cmul	$class \times$
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 (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x))$
23	1 6 22	cmpt	$class (x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
24	0 23	wceq	$wff arctan = (x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$

Metamath Proof Explorer

Definition df-atan

Detailed syntax breakdown