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

Metamath Proof Explorer

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