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

Metamath Proof Explorer

Theorem reexplog

Description: Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion reexplog ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( 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 eqtr2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) = ( exp ‘ ( 𝑁 · ( log ‘ 𝐴 ) ) ) )