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	|- ( ph -> B e. RR+ )
	relogbexpd.2	|- ( ph -> B =/= 1 )
	relogbexpd.3	|- ( ph -> M e. ZZ )
Assertion	relogbexpd	|- ( ph -> ( B logb ( B ^ M ) ) = M )

Proof

Step	Hyp	Ref	Expression
1		relogbexpd.1	|- ( ph -> B e. RR+ )
2		relogbexpd.2	|- ( ph -> B =/= 1 )
3		relogbexpd.3	|- ( ph -> M e. ZZ )
4	1 2 3	3jca	|- ( ph -> ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) )
5		relogbexp	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )
6	4 5	syl	|- ( ph -> ( B logb ( B ^ M ) ) = M )