MPE Home 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  tan ( z )  =/=  pm _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  pm _i; branch cuts are on the pure imaginary axis not between  -u _i 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.)
Assertion
Ref Expression
df-atan  |- arctan  =  ( x  e.  ( CC 
\  { -u _i ,  _i } )  |->  ( ( _i  /  2
)  x.  ( ( log `  ( 1  -  ( _i  x.  x ) ) )  -  ( log `  (
1  +  ( _i  x.  x ) ) ) ) ) )

Detailed syntax breakdown of Definition df-atan
StepHypRef Expression
1 catan 20706 . 2  class arctan
2 vx . . 3  set  x
3 cc 8990 . . . 4  class  CC
4 ci 8994 . . . . . 6  class  _i
54cneg 9294 . . . . 5  class  -u _i
65, 4cpr 3817 . . . 4  class  { -u _i ,  _i }
73, 6cdif 3319 . . 3  class  ( CC 
\  { -u _i ,  _i } )
8 c2 10051 . . . . 5  class  2
9 cdiv 9679 . . . . 5  class  /
104, 8, 9co 6083 . . . 4  class  ( _i 
/  2 )
11 c1 8993 . . . . . . 7  class  1
122cv 1652 . . . . . . . 8  class  x
13 cmul 8997 . . . . . . . 8  class  x.
144, 12, 13co 6083 . . . . . . 7  class  ( _i  x.  x )
15 cmin 9293 . . . . . . 7  class  -
1611, 14, 15co 6083 . . . . . 6  class  ( 1  -  ( _i  x.  x ) )
17 clog 20454 . . . . . 6  class  log
1816, 17cfv 5456 . . . . 5  class  ( log `  ( 1  -  (
_i  x.  x )
) )
19 caddc 8995 . . . . . . 7  class  +
2011, 14, 19co 6083 . . . . . 6  class  ( 1  +  ( _i  x.  x ) )
2120, 17cfv 5456 . . . . 5  class  ( log `  ( 1  +  ( _i  x.  x ) ) )
2218, 21, 15co 6083 . . . 4  class  ( ( log `  ( 1  -  ( _i  x.  x ) ) )  -  ( log `  (
1  +  ( _i  x.  x ) ) ) )
2310, 22, 13co 6083 . . 3  class  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) )
242, 7, 23cmpt 4268 . 2  class  ( x  e.  ( CC  \  { -u _i ,  _i } )  |->  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) ) )
251, 24wceq 1653 1  wff arctan  =  ( x  e.  ( CC 
\  { -u _i ,  _i } )  |->  ( ( _i  /  2
)  x.  ( ( log `  ( 1  -  ( _i  x.  x ) ) )  -  ( log `  (
1  +  ( _i  x.  x ) ) ) ) ) )
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