# Metamath Proof Explorer

## Theorem relogbmul

Description: The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 29-May-2020)

Ref Expression
Assertion relogbmul ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{A}{C}={\mathrm{log}}_{{B}}{A}+{\mathrm{log}}_{{B}}{C}$

### Proof

Step Hyp Ref Expression
1 relogmul ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to \mathrm{log}{A}{C}=\mathrm{log}{A}+\mathrm{log}{C}$
2 1 adantl ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to \mathrm{log}{A}{C}=\mathrm{log}{A}+\mathrm{log}{C}$
3 2 oveq1d ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to \frac{\mathrm{log}{A}{C}}{\mathrm{log}{B}}=\frac{\mathrm{log}{A}+\mathrm{log}{C}}{\mathrm{log}{B}}$
4 relogcl ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℝ$
5 4 recnd ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℂ$
6 5 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to \mathrm{log}{A}\in ℂ$
7 relogcl ${⊢}{C}\in {ℝ}^{+}\to \mathrm{log}{C}\in ℝ$
8 7 recnd ${⊢}{C}\in {ℝ}^{+}\to \mathrm{log}{C}\in ℂ$
9 8 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to \mathrm{log}{C}\in ℂ$
10 eldifpr ${⊢}{B}\in \left(ℂ\setminus \left\{0,1\right\}\right)↔\left({B}\in ℂ\wedge {B}\ne 0\wedge {B}\ne 1\right)$
11 3simpa ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\wedge {B}\ne 1\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
12 10 11 sylbi ${⊢}{B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
13 logcl ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to \mathrm{log}{B}\in ℂ$
14 12 13 syl ${⊢}{B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\to \mathrm{log}{B}\in ℂ$
15 logccne0 ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\wedge {B}\ne 1\right)\to \mathrm{log}{B}\ne 0$
16 10 15 sylbi ${⊢}{B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\to \mathrm{log}{B}\ne 0$
17 14 16 jca ${⊢}{B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\to \left(\mathrm{log}{B}\in ℂ\wedge \mathrm{log}{B}\ne 0\right)$
18 17 adantr ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to \left(\mathrm{log}{B}\in ℂ\wedge \mathrm{log}{B}\ne 0\right)$
19 divdir ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge \mathrm{log}{C}\in ℂ\wedge \left(\mathrm{log}{B}\in ℂ\wedge \mathrm{log}{B}\ne 0\right)\right)\to \frac{\mathrm{log}{A}+\mathrm{log}{C}}{\mathrm{log}{B}}=\left(\frac{\mathrm{log}{A}}{\mathrm{log}{B}}\right)+\left(\frac{\mathrm{log}{C}}{\mathrm{log}{B}}\right)$
20 6 9 18 19 syl2an23an ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to \frac{\mathrm{log}{A}+\mathrm{log}{C}}{\mathrm{log}{B}}=\left(\frac{\mathrm{log}{A}}{\mathrm{log}{B}}\right)+\left(\frac{\mathrm{log}{C}}{\mathrm{log}{B}}\right)$
21 3 20 eqtrd ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to \frac{\mathrm{log}{A}{C}}{\mathrm{log}{B}}=\left(\frac{\mathrm{log}{A}}{\mathrm{log}{B}}\right)+\left(\frac{\mathrm{log}{C}}{\mathrm{log}{B}}\right)$
22 rpcn ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℂ$
23 rpcn ${⊢}{C}\in {ℝ}^{+}\to {C}\in ℂ$
24 mulcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}\in ℂ$
25 22 23 24 syl2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}\in ℂ$
26 22 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}\in ℂ$
27 23 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {C}\in ℂ$
28 rpne0 ${⊢}{A}\in {ℝ}^{+}\to {A}\ne 0$
29 28 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}\ne 0$
30 rpne0 ${⊢}{C}\in {ℝ}^{+}\to {C}\ne 0$
31 30 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {C}\ne 0$
32 26 27 29 31 mulne0d ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}\ne 0$
33 eldifsn ${⊢}{A}{C}\in \left(ℂ\setminus \left\{0\right\}\right)↔\left({A}{C}\in ℂ\wedge {A}{C}\ne 0\right)$
34 25 32 33 sylanbrc ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}{C}\in \left(ℂ\setminus \left\{0\right\}\right)$
35 logbval ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge {A}{C}\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\mathrm{log}}_{{B}}{A}{C}=\frac{\mathrm{log}{A}{C}}{\mathrm{log}{B}}$
36 34 35 sylan2 ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{A}{C}=\frac{\mathrm{log}{A}{C}}{\mathrm{log}{B}}$
37 rpcndif0 ${⊢}{A}\in {ℝ}^{+}\to {A}\in \left(ℂ\setminus \left\{0\right\}\right)$
38 37 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {A}\in \left(ℂ\setminus \left\{0\right\}\right)$
39 logbval ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge {A}\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\mathrm{log}}_{{B}}{A}=\frac{\mathrm{log}{A}}{\mathrm{log}{B}}$
40 38 39 sylan2 ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{A}=\frac{\mathrm{log}{A}}{\mathrm{log}{B}}$
41 rpcndif0 ${⊢}{C}\in {ℝ}^{+}\to {C}\in \left(ℂ\setminus \left\{0\right\}\right)$
42 41 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to {C}\in \left(ℂ\setminus \left\{0\right\}\right)$
43 logbval ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge {C}\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\mathrm{log}}_{{B}}{C}=\frac{\mathrm{log}{C}}{\mathrm{log}{B}}$
44 42 43 sylan2 ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{C}=\frac{\mathrm{log}{C}}{\mathrm{log}{B}}$
45 40 44 oveq12d ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{A}+{\mathrm{log}}_{{B}}{C}=\left(\frac{\mathrm{log}{A}}{\mathrm{log}{B}}\right)+\left(\frac{\mathrm{log}{C}}{\mathrm{log}{B}}\right)$
46 21 36 45 3eqtr4d ${⊢}\left({B}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge \left({A}\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\right)\to {\mathrm{log}}_{{B}}{A}{C}={\mathrm{log}}_{{B}}{A}+{\mathrm{log}}_{{B}}{C}$