Theorem relogcl

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

	Ref	Expression
Assertion	relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐴 ) = ( log ‘ 𝐴 ) )
2		relogf1o	⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
3		f1of	⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
4	2 3	ax-mp	⊢ ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ
5	4	ffvelrni	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝐴 ) ∈ ℝ )
6	1 5	eqeltrrd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )