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

Definition df-log 23236
Description: Define the natural logarithm function on complex numbers. See http://en.wikipedia.org/wiki/Natural_logarithm ("The natural logarithm function can also be defined as the inverse function of the exponential function"). To obtain a function, only the principle value of the multivalued inverses of the exponential function, i.e. the inverse whose imaginary part lies in the interval (-pi, pi], see https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Paul Chapman, 21-Apr-2008.)
Assertion
Ref Expression
df-log  |-  log  =  `' ( exp  |`  ( `' Im " ( -u pi (,] pi ) ) )

Detailed syntax breakdown of Definition df-log
StepHypRef Expression
1 clog 23234 . 2  class  log
2 ce 14006 . . . 4  class  exp
3 cim 13080 . . . . . 6  class  Im
43ccnv 4822 . . . . 5  class  `' Im
5 cpi 14011 . . . . . . 7  class  pi
65cneg 9842 . . . . . 6  class  -u pi
7 cioc 11583 . . . . . 6  class  (,]
86, 5, 7co 6278 . . . . 5  class  ( -u pi (,] pi )
94, 8cima 4826 . . . 4  class  ( `' Im " ( -u pi (,] pi ) )
102, 9cres 4825 . . 3  class  ( exp  |`  ( `' Im "
( -u pi (,] pi ) ) )
1110ccnv 4822 . 2  class  `' ( exp  |`  ( `' Im " ( -u pi (,] pi ) ) )
121, 11wceq 1405 1  wff  log  =  `' ( exp  |`  ( `' Im " ( -u pi (,] pi ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  logrn  23238  dflog2  23240  dvlog  23326  efopnlem2  23332
  Copyright terms: Public domain W3C validator