Metamath Proof Explorer

Theorem relogbzexp

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. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 9-Jun-2020)

Ref Expression
Assertion relogbzexp 
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( C e. RR+ -> C e. CC )
2 1 adantr 
 |-  ( ( C e. RR+ /\ N e. ZZ ) -> C e. CC )
3 rpne0 
 |-  ( C e. RR+ -> C =/= 0 )
4 3 adantr 
 |-  ( ( C e. RR+ /\ N e. ZZ ) -> C =/= 0 )
5 simpr 
 |-  ( ( C e. RR+ /\ N e. ZZ ) -> N e. ZZ )
6 2 4 5 cxpexpzd 
 |-  ( ( C e. RR+ /\ N e. ZZ ) -> ( C ^c N ) = ( C ^ N ) )
7 6 3adant1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( C ^c N ) = ( C ^ N ) )
8 7 eqcomd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( C ^ N ) = ( C ^c N ) )
9 8 oveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( B logb ( C ^c N ) ) )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 relogbreexp 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. RR ) -> ( B logb ( C ^c N ) ) = ( N x. ( B logb C ) ) )
12 10 11 syl3an3 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^c N ) ) = ( N x. ( B logb C ) ) )
13 9 12 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) )