This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogcl

Description: Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007)

		Ref	Expression
	Assertion	relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$

Step	Hyp	Ref	Expression
1		fvres	$⊢ A \in ℝ^{+} \to ({log ↾}_{ℝ^{+}}) (A) = \log A$
2		relogf1o	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ$
3		f1of	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
4	2 3	ax-mp	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
5	4	ffvelcdmi	$⊢ A \in ℝ^{+} \to ({log ↾}_{ℝ^{+}}) (A) \in ℝ$
6	1 5	eqeltrrd	$⊢ A \in ℝ^{+} \to \log A \in ℝ$