Metamath Proof Explorer


Theorem reloggim

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 )

Proof

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 )