Theorem relogbzexpd

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, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	relogbzexpd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	relogbzexpd.2	⊢ ( 𝜑 → 𝐵 ≠ 1 )
	relogbzexpd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	relogbzexpd.4	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	relogbzexpd	⊢ ( 𝜑 → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		relogbzexpd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
2		relogbzexpd.2	⊢ ( 𝜑 → 𝐵 ≠ 1 )
3		relogbzexpd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4		relogbzexpd.4	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5	1	rpcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	1	rpne0d	⊢ ( 𝜑 → 𝐵 ≠ 0 )
7	6 2	nelprd	⊢ ( 𝜑 → ¬ 𝐵 ∈ { 0 , 1 } )
8	5 7	eldifd	⊢ ( 𝜑 → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
9	8 3 4	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) )
10		relogbzexp	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )
11	9 10	syl	⊢ ( 𝜑 → ( 𝐵 logb ( 𝐶 ↑ 𝑁 ) ) = ( 𝑁 · ( 𝐵 logb 𝐶 ) ) )