relogbmulbexp

Description: The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020)

		Ref	Expression
	Assertion	relogbmulbexp	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to \log_{B} A B^{C} = \log_{B} A + C$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
2	1	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in ℂ$
3		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
4	3	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 0$
5		simpr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 1$
6	2 4 5	3jca	$⊢ (B \in ℝ^{+} \land B \neq 1) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
7		eldifsn	$⊢ B \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (B \in ℝ^{+} \land B \neq 1)$
8		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
9	6 7 8	3imtr4i	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in (ℂ ∖ \{0, 1\})$
10	9	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to B \in (ℂ ∖ \{0, 1\})$
11		simprl	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to A \in ℝ^{+}$
12		eldifi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in ℝ^{+}$
13	12	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to B \in ℝ^{+}$
14		simpr	$⊢ (A \in ℝ^{+} \land C \in ℝ) \to C \in ℝ$
15	14	adantl	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to C \in ℝ$
16		relogbmulexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land B \in ℝ^{+} \land C \in ℝ)) \to \log_{B} A B^{C} = \log_{B} A + C \log_{B} B$
17	10 11 13 15 16	syl13anc	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to \log_{B} A B^{C} = \log_{B} A + C \log_{B} B$
18	7 6	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
19		logbid1	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log_{B} B = 1$
20	18 19	syl	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to \log_{B} B = 1$
21	20	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to \log_{B} B = 1$
22	21	oveq2d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to C \log_{B} B = C \cdot 1$
23		ax-1rid	$⊢ C \in ℝ \to C \cdot 1 = C$
24	23	adantl	$⊢ (A \in ℝ^{+} \land C \in ℝ) \to C \cdot 1 = C$
25	24	adantl	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to C \cdot 1 = C$
26	22 25	eqtrd	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to C \log_{B} B = C$
27	26	oveq2d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to \log_{B} A + C \log_{B} B = \log_{B} A + C$
28	17 27	eqtrd	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land (A \in ℝ^{+} \land C \in ℝ)) \to \log_{B} A B^{C} = \log_{B} A + C$

Metamath Proof Explorer

Theorem relogbmulbexp

Proof