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 ) |
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 ) |