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 ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( log ‘ ( 𝐴𝑁 ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 relogcl ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2 1 recnd ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
3 efexp ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) ↑ 𝑁 ) )
4 2 3 sylan ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) ↑ 𝑁 ) )
5 reeflog ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
6 5 oveq1d ( 𝐴 ∈ ℝ+ → ( ( exp ‘ ( log ‘ 𝐴 ) ) ↑ 𝑁 ) = ( 𝐴𝑁 ) )
7 6 adantr ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) ↑ 𝑁 ) = ( 𝐴𝑁 ) )
8 4 7 eqtrd ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) = ( 𝐴𝑁 ) )
9 8 fveq2d ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( log ‘ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ) = ( log ‘ ( 𝐴𝑁 ) ) )
10 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11 remulcl ( ( 𝑁 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ )
12 10 1 11 syl2anr ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ )
13 relogef ( ( 𝑁 · ( log ‘ 𝐴 ) ) ∈ ℝ → ( log ‘ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )
14 12 13 syl ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( log ‘ ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )
15 9 14 eqtr3d ( ( 𝐴 ∈ ℝ+𝑁 ∈ ℤ ) → ( log ‘ ( 𝐴𝑁 ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )