logmul2

Description: Generalization of relogmul to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017)

		Ref	Expression
	Assertion	logmul2	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log A B = \log A + \log B$

Proof

Step	Hyp	Ref	Expression
1		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
2	1	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log A \in ℂ$
3		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
4	3	3ad2ant3	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log B \in ℝ$
5	4	recnd	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log B \in ℂ$
6		efadd	$⊢ (\log A \in ℂ \land \log B \in ℂ) \to e^{\log A + \log B} = e^{\log A} e^{\log B}$
7	2 5 6	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to e^{\log A + \log B} = e^{\log A} e^{\log B}$
8		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
9	8	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to e^{\log A} = A$
10		reeflog	$⊢ B \in ℝ^{+} \to e^{\log B} = B$
11	10	3ad2ant3	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to e^{\log B} = B$
12	9 11	oveq12d	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to e^{\log A} e^{\log B} = A B$
13	7 12	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to e^{\log A + \log B} = A B$
14	13	fveq2d	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log e^{\log A + \log B} = \log A B$
15		logrncl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ran log$
16	15	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log A \in ran log$
17		logrnaddcl	$⊢ (\log A \in ran log \land \log B \in ℝ) \to \log A + \log B \in ran log$
18	16 4 17	syl2anc	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log A + \log B \in ran log$
19		logef	$⊢ \log A + \log B \in ran log \to \log e^{\log A + \log B} = \log A + \log B$
20	18 19	syl	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log e^{\log A + \log B} = \log A + \log B$
21	14 20	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℝ^{+}) \to \log A B = \log A + \log B$

Metamath Proof Explorer

Theorem logmul2

Proof