Theorem relogbzexp

Description: Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 9-Jun-2020)

	Ref	Expression
Assertion	relogbzexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝐶 ∈ ℂ )
3		rpne0	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ≠ 0 )
4	3	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝐶 ≠ 0 )
5		simpr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
6	2 4 5	cxpexpzd	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ↑𝑐 𝑁 ) = ( 𝐶 ↑ 𝑁 ) )
7	6	3adant1	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ↑𝑐 𝑁 ) = ( 𝐶 ↑ 𝑁 ) )
8	7	eqcomd	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ↑ 𝑁 ) = ( 𝐶 ↑𝑐 𝑁 ) )
9	8	oveq2d	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝐵 logb ( 𝐶 ↑𝑐 𝑁 ) ) )
10		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11		relogbreexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℝ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )
12	10 11	syl3an3	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 logb ( 𝐶 ↑𝑐 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )
13	9 12	eqtrd	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )