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