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 = ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		catan	⊢ arctan
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		ci	⊢ i
4	3	cneg	⊢ - i
5	4 3	cpr	⊢ { - i , i }
6	2 5	cdif	⊢ ( ℂ ∖ { - i , i } )
7		cdiv	⊢ /
8		c2	⊢ 2
9	3 8 7	co	⊢ ( i / 2 )
10		cmul	⊢ ·
11		clog	⊢ log
12		c1	⊢ 1
13		cmin	⊢ −
14	1	cv	⊢ 𝑥
15	3 14 10	co	⊢ ( i · 𝑥 )
16	12 15 13	co	⊢ ( 1 − ( i · 𝑥 ) )
17	16 11	cfv	⊢ ( log ‘ ( 1 − ( i · 𝑥 ) ) )
18		caddc	⊢ +
19	12 15 18	co	⊢ ( 1 + ( i · 𝑥 ) )
20	19 11	cfv	⊢ ( log ‘ ( 1 + ( i · 𝑥 ) ) )
21	17 20 13	co	⊢ ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) )
22	9 21 10	co	⊢ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) )
23	1 6 22	cmpt	⊢ ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )
24	0 23	wceq	⊢ arctan = ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Definition df-atan

Detailed syntax breakdown