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 Mario Carneiro, 29-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | relogcld.1 | |- ( ph -> A e. RR+ ) |
|
| relogmuld.2 | |- ( ph -> B e. RR+ ) |
||
| Assertion | relogmuld | |- ( ph -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relogcld.1 | |- ( ph -> A e. RR+ ) |
|
| 2 | relogmuld.2 | |- ( ph -> B e. RR+ ) |
|
| 3 | relogmul | |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) ) |
|
| 4 | 1 2 3 | syl2anc | |- ( ph -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) ) |