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

Definition df-atan 20163
Description: Define the arctangent function. See also remarks for df-asin 20161. 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 20160 . 2  class arctan
2 vx . . 3  set  x
3 cc 8735 . . . 4  class  CC
4 ci 8739 . . . . . 6  class  _i
54cneg 9038 . . . . 5  class  -u _i
65, 4cpr 3641 . . . 4  class  { -u _i ,  _i }
73, 6cdif 3149 . . 3  class  ( CC 
\  { -u _i ,  _i } )
8 c2 9795 . . . . 5  class  2
9 cdiv 9423 . . . . 5  class  /
104, 8, 9co 5858 . . . 4  class  ( _i 
/  2 )
11 c1 8738 . . . . . . 7  class  1
122cv 1622 . . . . . . . 8  class  x
13 cmul 8742 . . . . . . . 8  class  x.
144, 12, 13co 5858 . . . . . . 7  class  ( _i  x.  x )
15 cmin 9037 . . . . . . 7  class  -
1611, 14, 15co 5858 . . . . . 6  class  ( 1  -  ( _i  x.  x ) )
17 clog 19912 . . . . . 6  class  log
1816, 17cfv 5255 . . . . 5  class  ( log `  ( 1  -  (
_i  x.  x )
) )
19 caddc 8740 . . . . . . 7  class  +
2011, 14, 19co 5858 . . . . . 6  class  ( 1  +  ( _i  x.  x ) )
2120, 17cfv 5255 . . . . 5  class  ( log `  ( 1  +  ( _i  x.  x ) ) )
2218, 21, 15co 5858 . . . 4  class  ( ( log `  ( 1  -  ( _i  x.  x ) ) )  -  ( log `  (
1  +  ( _i  x.  x ) ) ) )
2310, 22, 13co 5858 . . 3  class  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) )
242, 7, 23cmpt 4077 . 2  class  ( x  e.  ( CC  \  { -u _i ,  _i } )  |->  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) ) )
251, 24wceq 1623 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  20172  atanf  20176  atanval  20180  dvatan  20231
  Copyright terms: Public domain W3C validator