Metamath Proof Explorer

Theorem reglogexp

Description: Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbzexp instead.

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

Proof

Step Hyp Ref Expression
1 relogexp 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )
2 1 3adant3 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )
3 2 oveq1d 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A ^ N ) ) / ( log ` C ) ) = ( ( N x. ( log ` A ) ) / ( log ` C ) ) )
4 zcn 
 |-  ( N e. ZZ -> N e. CC )
5 4 3ad2ant2 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> N e. CC )
6 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
7 6 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
8 7 3ad2ant1 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` A ) e. CC )
9 relogcl 
 |-  ( C e. RR+ -> ( log ` C ) e. RR )
10 9 recnd 
 |-  ( C e. RR+ -> ( log ` C ) e. CC )
11 10 adantr 
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) e. CC )
12 11 3ad2ant3 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` C ) e. CC )
13 logne0 
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) =/= 0 )
14 13 3ad2ant3 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( log ` C ) =/= 0 )
15 5 8 12 14 divassd 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( N x. ( log ` A ) ) / ( log ` C ) ) = ( N x. ( ( log ` A ) / ( log ` C ) ) ) )
16 3 15 eqtrd 
 |-  ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A ^ N ) ) / ( log ` C ) ) = ( N x. ( ( log ` A ) / ( log ` C ) ) ) )