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 e. RR+ -> ( log ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 fvres
 |-  ( A e. RR+ -> ( ( log |` RR+ ) ` A ) = ( log ` A ) )
2 relogf1o
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
3 f1of
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
4 2 3 ax-mp
 |-  ( log |` RR+ ) : RR+ --> RR
5 4 ffvelrni
 |-  ( A e. RR+ -> ( ( log |` RR+ ) ` A ) e. RR )
6 1 5 eqeltrrd
 |-  ( A e. RR+ -> ( log ` A ) e. RR )