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 24517
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 24515 . 2 class log
2 ce 15012 . . . 4 class exp
3 cim 14061 . . . . . 6 class
43ccnv 5310 . . . . 5 class
5 cpi 15017 . . . . . . 7 class π
65cneg 10552 . . . . . 6 class
7 cioc 12394 . . . . . 6 class (,]
86, 5, 7co 6874 . . . . 5 class (-π(,]π)
94, 8cima 5314 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5313 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5310 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1637 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
Colors of variables: wff setvar class
This definition is referenced by:  logrn  24519  dflog2  24521  dvlog  24611  efopnlem2  24617
  Copyright terms: Public domain W3C validator