Theorem logmul2

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

	Ref	Expression
Assertion	logmul2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
3		relogcl	⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
4	3	3ad2ant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ )
5	4	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℂ )
6		efadd	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐵 ) ) ) )
7	2 5 6	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐵 ) ) ) )
8		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
9	8	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
10		reeflog	⊢ ( 𝐵 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
11	10	3ad2ant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
12	9 11	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐵 ) ) ) = ( 𝐴 · 𝐵 ) )
13	7 12	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) = ( 𝐴 · 𝐵 ) )
14	13	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) ) = ( log ‘ ( 𝐴 · 𝐵 ) ) )
15		logrncl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )
16	15	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ran log )
17		logrnaddcl	⊢ ( ( ( log ‘ 𝐴 ) ∈ ran log ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ∈ ran log )
18	16 4 17	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ∈ ran log )
19		logef	⊢ ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
20	18 19	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
21	14 20	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )