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

Definition df-log 25067
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 25065 . 2 class log
2 ce 15405 . . . 4 class exp
3 cim 14447 . . . . . 6 class
43ccnv 5548 . . . . 5 class
5 cpi 15410 . . . . . . 7 class π
65cneg 10860 . . . . . 6 class
7 cioc 12729 . . . . . 6 class (,]
86, 5, 7co 7145 . . . . 5 class (-π(,]π)
94, 8cima 5552 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5551 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5548 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1528 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
Colors of variables: wff setvar class
This definition is referenced by:  logrn  25069  dflog2  25071  dvlog  25161  efopnlem2  25167
  Copyright terms: Public domain W3C validator