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

Metamath Proof Explorer

Theorem dflog2

Description: The natural logarithm function in terms of the exponential function restricted to its principal domain. (Contributed by Paul Chapman, 21-Apr-2008)

		Ref	Expression
	Assertion	dflog2	$⊢ log = {({\exp ↾}_{ran log})}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		df-log	$⊢ log = {({\exp ↾}_{ℑ^{-1} [(- π, π]]})}^{-1}$
2		logrn	$⊢ ran log = ℑ^{-1} [(- π, π]]$
3	2	reseq2i	$⊢ {\exp ↾}_{ran log} = {\exp ↾}_{ℑ^{-1} [(- π, π]]}$
4	3	cnveqi	$⊢ {({\exp ↾}_{ran log})}^{-1} = {({\exp ↾}_{ℑ^{-1} [(- π, π]]})}^{-1}$
5	1 4	eqtr4i	$⊢ log = {({\exp ↾}_{ran log})}^{-1}$