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

Definition df-atan 23786
 Description: Define the arctangent function. See also remarks for df-asin 23784. 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 23783 . 2 arctan
2 vx . . 3
3 cc 9534 . . . 4
4 ci 9538 . . . . . 6
54cneg 9858 . . . . 5
65, 4cpr 3969 . . . 4
73, 6cdif 3400 . . 3
8 c2 10656 . . . . 5
9 cdiv 10266 . . . . 5
104, 8, 9co 6288 . . . 4
11 c1 9537 . . . . . . 7
122cv 1442 . . . . . . . 8
13 cmul 9541 . . . . . . . 8
144, 12, 13co 6288 . . . . . . 7
15 cmin 9857 . . . . . . 7
1611, 14, 15co 6288 . . . . . 6
17 clog 23497 . . . . . 6
1816, 17cfv 5581 . . . . 5
19 caddc 9539 . . . . . . 7
2011, 14, 19co 6288 . . . . . 6
2120, 17cfv 5581 . . . . 5
2218, 21, 15co 6288 . . . 4
2310, 22, 13co 6288 . . 3
242, 7, 23cmpt 4460 . 2
251, 24wceq 1443 1 arctan
 Colors of variables: wff setvar class This definition is referenced by:  atandm  23795  atanf  23799  atanval  23803  dvatan  23854
 Copyright terms: Public domain W3C validator