Metamath Proof Explorer

Theorem logdiv2

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

Ref Expression
Assertion logdiv2 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 efsub ⊢ ( ( ( 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 2 5 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) + - ( log ‘ 𝐵 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )
16 logrncl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ran log )
18 4 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → - ( log ‘ 𝐵 ) ∈ ℝ )
19 logrnaddcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ran log ∧ - ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) + - ( log ‘ 𝐵 ) ) ∈ ran log )
20 17 18 19 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) + - ( log ‘ 𝐵 ) ) ∈ ran log )
21 15 20 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ∈ ran log )
22 logef ⊢ ( ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )
23 21 22 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( exp ‘ ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )
24 14 23 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝐵 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )