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 25151
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 25149 . 2 class log
2 ce 15410 . . . 4 class exp
3 cim 14452 . . . . . 6 class
43ccnv 5522 . . . . 5 class
5 cpi 15415 . . . . . . 7 class π
65cneg 10864 . . . . . 6 class
7 cioc 12731 . . . . . 6 class (,]
86, 5, 7co 7139 . . . . 5 class (-π(,]π)
94, 8cima 5526 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5525 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5522 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1538 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
Colors of variables: wff setvar class
This definition is referenced by:  logrn  25153  dflog2  25155  dvlog  25245  efopnlem2  25251
  Copyright terms: Public domain W3C validator