Theorem logef

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

	Ref	Expression
Assertion	logef	$$⊢A\in \mathrm{ran}log\to \log {\mathrm{e}}^A=A$$

Proof

Step	Hyp	Ref	Expression
1		dflog2	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
2	1	fveq1i	$$⊢\log \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)\right)$$
3		fvres	$$⊢A\in \mathrm{ran}log\to \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)={\mathrm{e}}^A$$
4	3	fveq2d	$$⊢A\in \mathrm{ran}log\to \log \left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)=\log {\mathrm{e}}^A$$
5		eff1o2	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$
6		f1ocnvfv1	$$⊢\left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\wedge A\in \mathrm{ran}log\right)\to {\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)\right)=A$$
7	5 6	mpan	$$⊢A\in \mathrm{ran}log\to {\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left(A\right)\right)=A$$
8	2 4 7	3eqtr3a	$$⊢A\in \mathrm{ran}log\to \log {\mathrm{e}}^A=A$$