This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridd 
 |-  ( ( 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 )