Theorem relogbmulbexp

Description: The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020)

	Ref	Expression
Assertion	relogbmulbexp	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐵 ↑𝑐 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
3		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
4	3	adantr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
5		simpr	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
6	2 4 5	3jca	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
7		eldifsn	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
8		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
9	6 7 8	3imtr4i	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
10	9	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
11		simprl	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ+ )
12		eldifi	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → 𝐵 ∈ ℝ+ )
13	12	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ+ )
14		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
15	14	adantl	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
16		relogbmulexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐵 ↑𝑐 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐶 · ( 𝐵 logb 𝐵 ) ) ) )
17	10 11 13 15 16	syl13anc	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐵 ↑𝑐 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐶 · ( 𝐵 logb 𝐵 ) ) ) )
18	7 6	sylbi	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
19		logbid1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝐵 ) = 1 )
20	18 19	syl	⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) → ( 𝐵 logb 𝐵 ) = 1 )
21	20	adantr	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 logb 𝐵 ) = 1 )
22	21	oveq2d	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 · ( 𝐵 logb 𝐵 ) ) = ( 𝐶 · 1 ) )
23		ax-1rid	⊢ ( 𝐶 ∈ ℝ → ( 𝐶 · 1 ) = 𝐶 )
24	23	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 · 1 ) = 𝐶 )
25	24	adantl	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 · 1 ) = 𝐶 )
26	22 25	eqtrd	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 · ( 𝐵 logb 𝐵 ) ) = 𝐶 )
27	26	oveq2d	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐵 logb 𝐴 ) + ( 𝐶 · ( 𝐵 logb 𝐵 ) ) ) = ( ( 𝐵 logb 𝐴 ) + 𝐶 ) )
28	17 27	eqtrd	⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐵 ↑𝑐 𝐶 ) ) ) = ( ( 𝐵 logb 𝐴 ) + 𝐶 ) )