Definition df-log 24303

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 |` ( `' Im " ( -u pi (,] pi ) ) )

Detailed syntax breakdown of Definition df-log

Step	Hyp	Ref	Expression
1		clog 24301	. 2 class log
2		ce 14792	. . . 4 class exp
3		cim 13838	. . . . . 6 class Im
4	3	ccnv 5113	. . . . 5 class `' Im
5		cpi 14797	. . . . . . 7 class pi
6	5	cneg 10267	. . . . . 6 class -u pi
7		cioc 12176	. . . . . 6 class (,]
8	6, 5, 7	co 6650	. . . . 5 class ( -u pi (,] pi )
9	4, 8	cima 5117	. . . 4 class ( `' Im " ( -u pi (,] pi ) )
10	2, 9	cres 5116	. . 3 class ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
11	10	ccnv 5113	. 2 class `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )
12	1, 11	wceq 1483	1 wff log = `' ( exp |` ( `' Im " ( -u pi (,] pi ) ) )

This definition is referenced by:  logrn  24305  dflog2  24307  dvlog  24397  efopnlem2  24403