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

Definition df-atan 20709
 Description: Define the arctangent function. See also remarks for df-asin 20707. 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
StepHypRef Expression
1 catan 20706 . 2 arctan
2 vx . . 3
3 cc 8990 . . . 4
4 ci 8994 . . . . . 6
54cneg 9294 . . . . 5
65, 4cpr 3817 . . . 4
73, 6cdif 3319 . . 3
8 c2 10051 . . . . 5
9 cdiv 9679 . . . . 5
104, 8, 9co 6083 . . . 4
11 c1 8993 . . . . . . 7
122cv 1652 . . . . . . . 8
13 cmul 8997 . . . . . . . 8
144, 12, 13co 6083 . . . . . . 7
15 cmin 9293 . . . . . . 7
1611, 14, 15co 6083 . . . . . 6
17 clog 20454 . . . . . 6
1816, 17cfv 5456 . . . . 5
19 caddc 8995 . . . . . . 7
2011, 14, 19co 6083 . . . . . 6
2120, 17cfv 5456 . . . . 5
2218, 21, 15co 6083 . . . 4
2310, 22, 13co 6083 . . 3
242, 7, 23cmpt 4268 . 2
251, 24wceq 1653 1 arctan
 Colors of variables: wff set class This definition is referenced by:  atandm  20718  atanf  20722  atanval  20726  dvatan  20777
 Copyright terms: Public domain W3C validator