df-atan - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-atan		Structured version Visualization version Unicode version

Definition df-atan 24594

Description: Define the arctangent function. See also remarks for df-asin 24592. Unlike arcsin and arccos, this function is not defined everywhere, because

for all

. For all other

, there is a formula for arctan

in terms of

, and we take that as the definition. Branch points are at

; branch cuts are on the pure imaginary axis not between

and

, which is to say

. (Contributed by Mario Carneiro, 31-Mar-2015.)

**Assertion**
Ref	Expression
df-atan	arctan $\$

**Detailed syntax breakdown of Definition df-atan**
Step	Hyp	Ref	Expression
1		catan 24591	. 2 arctan
2		vx	. . 3
3		cc 9934	. . . 4
4		ci 9938	. . . . . 6
5	4	cneg 10267	. . . . 5
6	5, 4	cpr 4179	. . . 4
7	3, 6	cdif 3571	. . 3 $\$
8		c2 11070	. . . . 5
9		cdiv 10684	. . . . 5
10	4, 8, 9	co 6650	. . . 4
11		c1 9937	. . . . . . 7
12	2	cv 1482	. . . . . . . 8
13		cmul 9941	. . . . . . . 8
14	4, 12, 13	co 6650	. . . . . . 7
15		cmin 10266	. . . . . . 7
16	11, 14, 15	co 6650	. . . . . 6
17		clog 24301	. . . . . 6
18	16, 17	cfv 5888	. . . . 5
19		caddc 9939	. . . . . . 7
20	11, 14, 19	co 6650	. . . . . 6
21	20, 17	cfv 5888	. . . . 5
22	18, 21, 15	co 6650	. . . 4
23	10, 22, 13	co 6650	. . 3
24	2, 7, 23	cmpt 4729	. 2 $\$
25	1, 24	wceq 1483	1 arctan $\$

Colors of variables: wff setvar class

This definition is referenced by: atandm 24603 atanf 24607 atanval 24611 dvatan 24662

W3C validator