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	$$⊢\phi \to B\in {ℝ}^{+}$$
	relogbzexpd.2	$$⊢\phi \to B\ne 1$$
	relogbzexpd.3	$$⊢\phi \to C\in {ℝ}^{+}$$
	relogbzexpd.4	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	relogbzexpd	$$⊢\phi \to {\log }_B{C}^N=N{\log }_{B}C$$

Proof

Step	Hyp	Ref	Expression
1		relogbzexpd.1	$$⊢\phi \to B\in {ℝ}^{+}$$
2		relogbzexpd.2	$$⊢\phi \to B\ne 1$$
3		relogbzexpd.3	$$⊢\phi \to C\in {ℝ}^{+}$$
4		relogbzexpd.4	$$⊢\phi \to N\in \mathbb{Z}$$
5	1	rpcnd	$$⊢\phi \to B\in ℂ$$
6	1	rpne0d	$$⊢\phi \to B\ne 0$$
7	6 2	nelprd	$$⊢\phi \to \neg B\in \left\{0,1\right\}$$
8	5 7	eldifd	$$⊢\phi \to B\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
9	8 3 4	3jca	$$⊢\phi \to \left(B\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge C\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)$$
10		relogbzexp	$$⊢\left(B\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge C\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to {\log }_B{C}^N=N{\log }_{B}C$$
11	9 10	syl	$$⊢\phi \to {\log }_B{C}^N=N{\log }_{B}C$$