Theorem relogbmulexp

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

	Ref	Expression
Assertion	relogbmulexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶 ↑𝑐 𝐸 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐸 · ( 𝐵 logb 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → 𝐴 ∈ ℝ+ )
2		rpcxpcl	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ∈ ℝ+ )
3	2	3adant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐶 ↑𝑐 𝐸 ) ∈ ℝ+ )
4	1 3	jca	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐴 ∈ ℝ+ ∧ ( 𝐶 ↑𝑐 𝐸 ) ∈ ℝ+ ) )
5		relogbmul	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ ( 𝐶 ↑𝑐 𝐸 ) ∈ ℝ+ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶 ↑𝑐 𝐸 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) ) )
6	4 5	sylan2	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶 ↑𝑐 𝐸 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) ) )
7		relogbreexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( 𝐵 logb 𝐶 ) ) )
8	7	3adant3r1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) = ( 𝐸 · ( 𝐵 logb 𝐶 ) ) )
9	8	oveq2d	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) ) → ( ( 𝐵 logb 𝐴 ) + ( 𝐵 logb ( 𝐶 ↑𝑐 𝐸 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐸 · ( 𝐵 logb 𝐶 ) ) ) )
10	6 9	eqtrd	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ ) ) → ( 𝐵 logb ( 𝐴 · ( 𝐶 ↑𝑐 𝐸 ) ) ) = ( ( 𝐵 logb 𝐴 ) + ( 𝐸 · ( 𝐵 logb 𝐶 ) ) ) )