This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogbmul

Description: The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 29-May-2020)

Ref Expression
Assertion relogbmul ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 · 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 relogmul ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐶 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐶 ) ) )
2 1 adantl ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( log ‘ ( 𝐴 · 𝐶 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐶 ) ) )
3 2 oveq1d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( ( log ‘ ( 𝐴 · 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) )
4 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
5 4 recnd ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
7 relogcl ⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℝ )
8 7 recnd ⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℂ )
9 8 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( log ‘ 𝐶 ) ∈ ℂ )
10 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
11 3simpa ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
12 10 11 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
13 logcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
14 12 13 syl ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ∈ ℂ )
15 logccne0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
16 10 15 sylbi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( log ‘ 𝐵 ) ≠ 0 )
17 14 16 jca ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
18 17 adantr ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) )
19 divdir ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐶 ) ∈ ℂ ∧ ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) + ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
20 6 9 18 19 syl2an23an ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( ( ( log ‘ 𝐴 ) + ( log ‘ 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) + ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
21 3 20 eqtrd ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( ( log ‘ ( 𝐴 · 𝐶 ) ) / ( log ‘ 𝐵 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) + ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
22 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
23 rpcn ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℂ )
24 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
25 22 23 24 syl2an ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
26 22 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
27 23 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
28 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
29 28 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ≠ 0 )
30 rpne0 ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ≠ 0 )
31 30 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ≠ 0 )
32 26 27 29 31 mulne0d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐶 ) ≠ 0 )
33 eldifsn ⊢ ( ( 𝐴 · 𝐶 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ≠ 0 ) )
34 25 32 33 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐶 ) ∈ ( ℂ ∖ { 0 } ) )
35 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 · 𝐶 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb ( 𝐴 · 𝐶 ) ) = ( ( log ‘ ( 𝐴 · 𝐶 ) ) / ( log ‘ 𝐵 ) ) )
36 34 35 sylan2 ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 · 𝐶 ) ) = ( ( log ‘ ( 𝐴 · 𝐶 ) ) / ( log ‘ 𝐵 ) ) )
37 rpcndif0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
38 37 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
39 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
40 38 39 sylan2 ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
41 rpcndif0 ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
42 41 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
43 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐶 ) = ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) )
44 42 43 sylan2 ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb 𝐶 ) = ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) )
45 40 44 oveq12d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb 𝐶 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) + ( ( log ‘ 𝐶 ) / ( log ‘ 𝐵 ) ) ) )
46 21 36 45 3eqtr4d ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 · 𝐶 ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb 𝐶 ) ) )