Metamath Proof Explorer

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 ‘ 𝐵 ) ) )