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 24348
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 24346 . 2 class log
2 ce 14836 . . . 4 class exp
3 cim 13882 . . . . . 6 class
43ccnv 5142 . . . . 5 class
5 cpi 14841 . . . . . . 7 class π
65cneg 10305 . . . . . 6 class
7 cioc 12214 . . . . . 6 class (,]
86, 5, 7co 6690 . . . . 5 class (-π(,]π)
94, 8cima 5146 . . . 4 class (ℑ “ (-π(,]π))
102, 9cres 5145 . . 3 class (exp ↾ (ℑ “ (-π(,]π)))
1110ccnv 5142 . 2 class (exp ↾ (ℑ “ (-π(,]π)))
121, 11wceq 1523 1 wff log = (exp ↾ (ℑ “ (-π(,]π)))
Colors of variables: wff setvar class
This definition is referenced by:  logrn  24350  dflog2  24352  dvlog  24442  efopnlem2  24448
  Copyright terms: Public domain W3C validator