Theorem eflog

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$

Proof

Step	Hyp	Ref	Expression
1		dflog2	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
2	1	fveq1i	$$⊢\log A={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(A\right)$$
3	2	fveq2i	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(\log A\right)=\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(A\right)\right)$$
4		logrncl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in \mathrm{ran}log$$
5	4	fvresd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(\log A\right)={\mathrm{e}}^{\log A}$$
6		eldifsn	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(A\in ℂ\wedge A\ne 0\right)$$
7		eff1o2	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$
8		f1ocnvfv2	$$⊢\left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\wedge A\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(A\right)\right)=A$$
9	7 8	mpan	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(A\right)\right)=A$$
10	6 9	sylbir	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(A\right)\right)=A$$
11	3 5 10	3eqtr3a	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$