Metamath Proof Explorer

Theorem reglogmul

Description: Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbmul instead.

		Ref	Expression
	Assertion	reglogmul	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A B}{\log C} = (\frac{\log A}{\log C}) + (\frac{\log B}{\log C})$

Proof

Step	Hyp	Ref	Expression
1		relogmul	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \log A B = \log A + \log B$
2	1	3adant3	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \log A B = \log A + \log B$
3	2	oveq1d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A B}{\log C} = \frac{\log A + \log B}{\log C}$
4		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
5	4	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
6	5	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \log A \in ℂ$
7		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
8	7	recnd	$⊢ B \in ℝ^{+} \to \log B \in ℂ$
9	8	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \log B \in ℂ$
10		relogcl	$⊢ C \in ℝ^{+} \to \log C \in ℝ$
11	10	recnd	$⊢ C \in ℝ^{+} \to \log C \in ℂ$
12	11	adantr	$⊢ (C \in ℝ^{+} \land C \neq 1) \to \log C \in ℂ$
13	12	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \log C \in ℂ$
14		logne0	$⊢ (C \in ℝ^{+} \land C \neq 1) \to \log C \neq 0$
15	14	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \log C \neq 0$
16	6 9 13 15	divdird	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A + \log B}{\log C} = (\frac{\log A}{\log C}) + (\frac{\log B}{\log C})$
17	3 16	eqtrd	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+} \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A B}{\log C} = (\frac{\log A}{\log C}) + (\frac{\log B}{\log C})$