Definition df-log

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)

	Ref	Expression
Assertion	df-log	|- log = `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clog	|- log
1		ce	|- exp
2		cim	|- Im
3	2	ccnv	|- `' Im
4		cpi	|- _pi
5	4	cneg	|- -u _pi
6		cioc	|- (,]
7	5 4 6	co	|- ( -u _pi (,] _pi )
8	3 7	cima	|- ( `' Im " ( -u _pi (,] _pi ) )
9	1 8	cres	|- ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
10	9	ccnv	|- `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
11	0 10	wceq	|- log = `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )