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 ℝ$$

Proof

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