Metamath Proof Explorer

Theorem relogcn

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

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

Proof

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