Definition df-log 24107

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	⊢ log = ◡(exp ↾ (◡ℑ “ (-π(,]π)))

Detailed syntax breakdown of Definition df-log

Step	Hyp	Ref	Expression
1		clog 24105	. 2 class log
2		ce 14631	. . . 4 class exp
3		cim 13686	. . . . . 6 class ℑ
4	3	ccnv 5037	. . . . 5 class ◡ℑ
5		cpi 14636	. . . . . . 7 class π
6	5	cneg 10146	. . . . . 6 class -π
7		cioc 12047	. . . . . 6 class (,]
8	6, 5, 7	co 6549	. . . . 5 class (-π(,]π)
9	4, 8	cima 5041	. . . 4 class (◡ℑ “ (-π(,]π))
10	2, 9	cres 5040	. . 3 class (exp ↾ (◡ℑ “ (-π(,]π)))
11	10	ccnv 5037	. 2 class ◡(exp ↾ (◡ℑ “ (-π(,]π)))
12	1, 11	wceq 1475	1 wff log = ◡(exp ↾ (◡ℑ “ (-π(,]π)))

This definition is referenced by:  logrn  24109  dflog2  24111  dvlog  24197  efopnlem2  24203