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={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clog	$$classlog$$
1		ce	$$class\exp$$
2		cim	$$class\Im$$
3	2	ccnv	$$class{\Im }^{-1}$$
4		cpi	$$class\mathrm{\pi }$$
5	4	cneg	$$class\left(-\mathrm{\pi }\right)$$
6		cioc	$$class\left(.\right]$$
7	5 4 6	co	$$class\left(-\mathrm{\pi },\mathrm{\pi }\right]$$
8	3 7	cima	$$class{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
9	1 8	cres	$$class\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)$$
10	9	ccnv	$$class{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$
11	0 10	wceq	$$wfflog={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$