relogbmulexp

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

		Ref	Expression
	Assertion	relogbmulexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ)) \to \log_{B} A C^{E} = \log_{B} A + E \log_{B} C$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ) \to A \in ℝ^{+}$
2		rpcxpcl	$⊢ (C \in ℝ^{+} \land E \in ℝ) \to C^{E} \in ℝ^{+}$
3	2	3adant1	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ) \to C^{E} \in ℝ^{+}$
4	1 3	jca	$⊢ (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ) \to (A \in ℝ^{+} \land C^{E} \in ℝ^{+})$
5		relogbmul	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C^{E} \in ℝ^{+})) \to \log_{B} A C^{E} = \log_{B} A + \log_{B} C^{E}$
6	4 5	sylan2	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ)) \to \log_{B} A C^{E} = \log_{B} A + \log_{B} C^{E}$
7		relogbreexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land C \in ℝ^{+} \land E \in ℝ) \to \log_{B} C^{E} = E \log_{B} C$
8	7	3adant3r1	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ)) \to \log_{B} C^{E} = E \log_{B} C$
9	8	oveq2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ)) \to \log_{B} A + \log_{B} C^{E} = \log_{B} A + E \log_{B} C$
10	6 9	eqtrd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land (A \in ℝ^{+} \land C \in ℝ^{+} \land E \in ℝ)) \to \log_{B} A C^{E} = \log_{B} A + E \log_{B} C$

Metamath Proof Explorer

Theorem relogbmulexp

Proof