Theorem relogbexp

Description: Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 9-Jun-2020)

	Ref	Expression
Assertion	relogbexp	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )

Proof

Step	Hyp	Ref	Expression
1		rpcn	|- ( B e. RR+ -> B e. CC )
2	1	adantr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B e. CC )
3		rpne0	|- ( B e. RR+ -> B =/= 0 )
4	3	adantr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 0 )
5		simpr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 1 )
6	2 4 5	3jca	|- ( ( B e. RR+ /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
7		eldifpr	|- ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
8	6 7	sylibr	|- ( ( B e. RR+ /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
9		relogbzexp	|- ( ( B e. ( CC \ { 0 , 1 } ) /\ B e. RR+ /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = ( M x. ( B logb B ) ) )
10	8 9	stoic4a	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = ( M x. ( B logb B ) ) )
11	6	3adant3	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
12		logbid1	|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb B ) = 1 )
13	11 12	syl	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb B ) = 1 )
14	13	oveq2d	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( M x. ( B logb B ) ) = ( M x. 1 ) )
15		zcn	|- ( M e. ZZ -> M e. CC )
16	15	3ad2ant3	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> M e. CC )
17	16	mulid1d	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( M x. 1 ) = M )
18	10 14 17	3eqtrd	|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )