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

Definition df-log 23506
 Description: Define the natural logarithm function on complex numbers. See http://en.wikipedia.org/wiki/Natural_logarithm ("The natural logarithm function can also be defined as the inverse function of the exponential function"). To obtain a function, only the principle value of the multivalued inverses of the exponential function, i.e. the inverse whose imaginary part lies in the interval (-pi, pi], see https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Paul Chapman, 21-Apr-2008.)
Assertion
Ref Expression
df-log

Detailed syntax breakdown of Definition df-log
StepHypRef Expression
1 clog 23504 . 2
2 ce 14114 . . . 4
3 cim 13161 . . . . . 6
43ccnv 4833 . . . . 5
5 cpi 14119 . . . . . . 7
65cneg 9861 . . . . . 6
7 cioc 11636 . . . . . 6
86, 5, 7co 6290 . . . . 5
94, 8cima 4837 . . . 4
102, 9cres 4836 . . 3
1110ccnv 4833 . 2
121, 11wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  logrn  23508  dflog2  23510  dvlog  23596  efopnlem2  23602
 Copyright terms: Public domain W3C validator