Theorem relogbexpd

Description: Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	relogbexpd.1	$$⊢\phi \to B\in {ℝ}^{+}$$
	relogbexpd.2	$$⊢\phi \to B\ne 1$$
	relogbexpd.3	$$⊢\phi \to M\in \mathbb{Z}$$
Assertion	relogbexpd	$$⊢\phi \to {\log }_B{B}^M=M$$

Proof

Step	Hyp	Ref	Expression
1		relogbexpd.1	$$⊢\phi \to B\in {ℝ}^{+}$$
2		relogbexpd.2	$$⊢\phi \to B\ne 1$$
3		relogbexpd.3	$$⊢\phi \to M\in \mathbb{Z}$$
4	1 2 3	3jca	$$⊢\phi \to \left(B\in {ℝ}^{+}\wedge B\ne 1\wedge M\in \mathbb{Z}\right)$$
5		relogbexp	$$⊢\left(B\in {ℝ}^{+}\wedge B\ne 1\wedge M\in \mathbb{Z}\right)\to {\log }_B{B}^M=M$$
6	4 5	syl	$$⊢\phi \to {\log }_B{B}^M=M$$