Description: The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of Cohen p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | relogmul | |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efadd | |- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) + ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( log ` B ) ) ) ) |
|
2 | readdcl | |- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) + ( log ` B ) ) e. RR ) |
|
3 | 1 2 | relogoprlem | |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) ) |