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

Definition df-log 24107
 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 ↾ (ℑ “ (-π(,]π)))

Detailed syntax breakdown of Definition df-log
StepHypRef Expression
1 clog 24105 . 2 class log
2 ce 14631 . . . 4 class exp
3 cim 13686 . . . . . 6 class
43ccnv 5037 . . . . 5 class
5 cpi 14636 . . . . . . 7 class π
65cneg 10146 . . . . . 6 class
7 cioc 12047 . . . . . 6 class (,]
86, 5, 7co 6549 . . . . 5 class (-π(,]π)
94, 8cima 5041 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5040 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5037 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1475 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
 Colors of variables: wff setvar class This definition is referenced by:  logrn  24109  dflog2  24111  dvlog  24197  efopnlem2  24203
 Copyright terms: Public domain W3C validator