Theorem dfrelog

Description: The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	dfrelog	$$⊢{log\upharpoonright }_{{ℝ}^{+}}={\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]=\mathrm{ran}\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right)$$
2		relogrn	$$⊢x\in ℝ\to x\in \mathrm{ran}log$$
3	2	ssriv	$$⊢ℝ\subseteq \mathrm{ran}log$$
4		resabs1	$$⊢ℝ\subseteq \mathrm{ran}log\to {\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}={\exp \upharpoonright }_{ℝ}$$
5	3 4	ax-mp	$$⊢{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}={\exp \upharpoonright }_{ℝ}$$
6	5	rneqi	$$⊢\mathrm{ran}\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right)=\mathrm{ran}\left({\exp \upharpoonright }_{ℝ}\right)$$
7		reeff1o	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}$$
8		dff1o2	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\leftrightarrow \left(\left({\exp \upharpoonright }_{ℝ}\right)Fnℝ\wedge \mathrm{Fun}{\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}\wedge \mathrm{ran}\left({\exp \upharpoonright }_{ℝ}\right)={ℝ}^{+}\right)$$
9	7 8	mpbi	$$⊢\left(\left({\exp \upharpoonright }_{ℝ}\right)Fnℝ\wedge \mathrm{Fun}{\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}\wedge \mathrm{ran}\left({\exp \upharpoonright }_{ℝ}\right)={ℝ}^{+}\right)$$
10	9	simp3i	$$⊢\mathrm{ran}\left({\exp \upharpoonright }_{ℝ}\right)={ℝ}^{+}$$
11	1 6 10	3eqtri	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]={ℝ}^{+}$$
12	11	reseq2i	$$⊢{{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}$$
13	5	cnveqi	$$⊢{\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right)}^{-1}={\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}$$
14		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
15		f1ofun	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to \mathrm{Fun}log$$
16	14 15	ax-mp	$$⊢\mathrm{Fun}log$$
17		dflog2	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
18	17	funeqi	$$⊢\mathrm{Fun}log\leftrightarrow \mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
19	16 18	mpbi	$$⊢\mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
20		funcnvres	$$⊢\mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\to {\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right)}^{-1}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]}$$
21	19 20	ax-mp	$$⊢{\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right)}^{-1}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]}$$
22	13 21	eqtr3i	$$⊢{\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\left[ℝ\right]}$$
23	17	reseq1i	$$⊢{log\upharpoonright }_{{ℝ}^{+}}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}$$
24	12 22 23	3eqtr4ri	$$⊢{log\upharpoonright }_{{ℝ}^{+}}={\left({\exp \upharpoonright }_{ℝ}\right)}^{-1}$$