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

Definition df-log 24857
 Description: Define the natural logarithm function on complex numbers. It is defined as the principal value, that is, the inverse of the exponential whose imaginary part lies in the interval (-pi, pi]. See http://en.wikipedia.org/wiki/Natural_logarithm and 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 24855 . 2 class log
2 ce 15274 . . . 4 class exp
3 cim 14317 . . . . . 6 class
43ccnv 5403 . . . . 5 class
5 cpi 15279 . . . . . . 7 class π
65cneg 10670 . . . . . 6 class
7 cioc 12554 . . . . . 6 class (,]
86, 5, 7co 6975 . . . . 5 class (-π(,]π)
94, 8cima 5407 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5406 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5403 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1508 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
 Colors of variables: wff setvar class This definition is referenced by:  logrn  24859  dflog2  24861  dvlog  24951  efopnlem2  24957
 Copyright terms: Public domain W3C validator