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

Definition df-atan 20179
Description: Define the arctangent function. See also remarks for df-asin 20177. 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 20176 . 2  class arctan
2 vx . . 3  set  x
3 cc 8751 . . . 4  class  CC
4 ci 8755 . . . . . 6  class  _i
54cneg 9054 . . . . 5  class  -u _i
65, 4cpr 3654 . . . 4  class  { -u _i ,  _i }
73, 6cdif 3162 . . 3  class  ( CC 
\  { -u _i ,  _i } )
8 c2 9811 . . . . 5  class  2
9 cdiv 9439 . . . . 5  class  /
104, 8, 9co 5874 . . . 4  class  ( _i 
/  2 )
11 c1 8754 . . . . . . 7  class  1
122cv 1631 . . . . . . . 8  class  x
13 cmul 8758 . . . . . . . 8  class  x.
144, 12, 13co 5874 . . . . . . 7  class  ( _i  x.  x )
15 cmin 9053 . . . . . . 7  class  -
1611, 14, 15co 5874 . . . . . 6  class  ( 1  -  ( _i  x.  x ) )
17 clog 19928 . . . . . 6  class  log
1816, 17cfv 5271 . . . . 5  class  ( log `  ( 1  -  (
_i  x.  x )
) )
19 caddc 8756 . . . . . . 7  class  +
2011, 14, 19co 5874 . . . . . 6  class  ( 1  +  ( _i  x.  x ) )
2120, 17cfv 5271 . . . . 5  class  ( log `  ( 1  +  ( _i  x.  x ) ) )
2218, 21, 15co 5874 . . . 4  class  ( ( log `  ( 1  -  ( _i  x.  x ) ) )  -  ( log `  (
1  +  ( _i  x.  x ) ) ) )
2310, 22, 13co 5874 . . 3  class  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) )
242, 7, 23cmpt 4093 . 2  class  ( x  e.  ( CC  \  { -u _i ,  _i } )  |->  ( ( _i  /  2 )  x.  ( ( log `  ( 1  -  (
_i  x.  x )
) )  -  ( log `  ( 1  +  ( _i  x.  x
) ) ) ) ) )
251, 24wceq 1632 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  20188  atanf  20192  atanval  20196  dvatan  20247
  Copyright terms: Public domain W3C validator