Theorem relogcn

Description: The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Assertion	relogcn	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		relogf1o	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
2		f1of	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
3	1 2	ax-mp	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5		fss	$$⊢\left(\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℂ$$
6	3 4 5	mp2an	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℂ$$
7		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
8		ovex	$$⊢\frac{1}{x}\in \mathrm{V}$$
9		dvrelog	$$⊢ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
10	8 9	dmmpti	$$⊢\mathrm{dom}{\left({log\upharpoonright }_{{ℝ}^{+}}\right)}_{ℝ}^{\prime }={ℝ}^{+}$$
11		dvcn	$$⊢\left(\left(ℝ\subseteq ℂ\wedge \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℂ\wedge {ℝ}^{+}\subseteq ℝ\right)\wedge \mathrm{dom}{\left({log\upharpoonright }_{{ℝ}^{+}}\right)}_{ℝ}^{\prime }={ℝ}^{+}\right)\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ$$
12	10 11	mpan2	$$⊢\left(ℝ\subseteq ℂ\wedge \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℂ\wedge {ℝ}^{+}\subseteq ℝ\right)\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ$$
13	4 6 7 12	mp3an	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ$$
14		cncffvrn	$$⊢\left(ℝ\subseteq ℂ\wedge \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℂ\right)\to \left(\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ\leftrightarrow \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ\right)$$
15	4 13 14	mp2an	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ\leftrightarrow \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
16	3 15	mpbir	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ$$