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

Metamath Proof Explorer

Theorem relogexp

Description: The natural logarithm of positive A raised to an integer power. Property 4 of Cohen p. 301-302, restricted to natural logarithms and integer powers N . (Contributed by Steve Rodriguez, 25-Nov-2007)

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

Proof

Step Hyp Ref Expression
1 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
2 1 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
3 efexp 
 |-  ( ( ( log ` A ) e. CC /\ N e. ZZ ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( ( exp ` ( log ` A ) ) ^ N ) )
4 2 3 sylan 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( ( exp ` ( log ` A ) ) ^ N ) )
5 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
6 5 oveq1d 
 |-  ( A e. RR+ -> ( ( exp ` ( log ` A ) ) ^ N ) = ( A ^ N ) )
7 6 adantr 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( ( exp ` ( log ` A ) ) ^ N ) = ( A ^ N ) )
8 4 7 eqtrd 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( A ^ N ) )
9 8 fveq2d 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( exp ` ( N x. ( log ` A ) ) ) ) = ( log ` ( A ^ N ) ) )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 remulcl 
 |-  ( ( N e. RR /\ ( log ` A ) e. RR ) -> ( N x. ( log ` A ) ) e. RR )
12 10 1 11 syl2anr 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( N x. ( log ` A ) ) e. RR )
13 relogef 
 |-  ( ( N x. ( log ` A ) ) e. RR -> ( log ` ( exp ` ( N x. ( log ` A ) ) ) ) = ( N x. ( log ` A ) ) )
14 12 13 syl 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( exp ` ( N x. ( log ` A ) ) ) ) = ( N x. ( log ` A ) ) )
15 9 14 eqtr3d 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )