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 ( 𝐴 ∈ ℝ+ → ( 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 ‘ 𝐴 ) ∈ ℝ )