This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾}_{ℑ^{-1} [(- π, π]]})}^{-1}$

Step	Hyp	Ref	Expression
0		clog	$class log$
1		ce	$class \exp$
2		cim	$class ℑ$
3	2	ccnv	$class ℑ^{-1}$
4		cpi	$class π$
5	4	cneg	$class (- π)$
6		cioc	$class (.]$
7	5 4 6	co	$class (- π, π]$
8	3 7	cima	$class ℑ^{-1} [(- π, π]]$
9	1 8	cres	$class ({\exp ↾}_{ℑ^{-1} [(- π, π]]})$
10	9	ccnv	$class {({\exp ↾}_{ℑ^{-1} [(- π, π]]})}^{-1}$
11	0 10	wceq	$wff log = {({\exp ↾}_{ℑ^{-1} [(- π, π]]})}^{-1}$