Metamath Proof Explorer

Theorem reglogexpbas

Description: General log of a power of the base is the exponent. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbexp instead.

Ref Expression
Assertion reglogexpbas 
|- ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( C ^ N ) ) / ( log ` C ) ) = N )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> C e. RR+ )
2 simpl 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> N e. ZZ )
3 simpr 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( C e. RR+ /\ C =/= 1 ) )
4 reglogexp 
 |-  ( ( C e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( C ^ N ) ) / ( log ` C ) ) = ( N x. ( ( log ` C ) / ( log ` C ) ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( C ^ N ) ) / ( log ` C ) ) = ( N x. ( ( log ` C ) / ( log ` C ) ) ) )
6 reglogbas 
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )
7 6 adantl 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )
8 7 oveq2d 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( N x. ( ( log ` C ) / ( log ` C ) ) ) = ( N x. 1 ) )
9 zcn 
 |-  ( N e. ZZ -> N e. CC )
10 9 adantr 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> N e. CC )
11 10 mulid1d 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( N x. 1 ) = N )
12 5 8 11 3eqtrd 
 |-  ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( C ^ N ) ) / ( log ` C ) ) = N )