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