Description: The natural logarithm is a group isomorphism from the group of positive reals under multiplication to the group of reals under addition. (Contributed by Mario Carneiro, 21-Jun-2015) (Revised by Thierry Arnoux, 30-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | reloggim.1 | |- P = ( ( mulGrp ` CCfld ) |`s RR+ ) |
|
Assertion | reloggim | |- ( log |` RR+ ) e. ( P GrpIso RRfld ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reloggim.1 | |- P = ( ( mulGrp ` CCfld ) |`s RR+ ) |
|
2 | dfrelog | |- ( log |` RR+ ) = `' ( exp |` RR ) |
|
3 | 1 | reefgim | |- ( exp |` RR ) e. ( RRfld GrpIso P ) |
4 | gimcnv | |- ( ( exp |` RR ) e. ( RRfld GrpIso P ) -> `' ( exp |` RR ) e. ( P GrpIso RRfld ) ) |
|
5 | 3 4 | ax-mp | |- `' ( exp |` RR ) e. ( P GrpIso RRfld ) |
6 | 2 5 | eqeltri | |- ( log |` RR+ ) e. ( P GrpIso RRfld ) |