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	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+})) \to \log_{B} A C = \log_{B} A + \log_{B} C$

Proof

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

Metamath Proof Explorer

Theorem relogbmul

Proof