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 𝐶 ) ) )