# 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 ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {{A}}^{{N}}={\mathrm{e}}^{{N}\mathrm{log}{A}}$

### Proof

Step Hyp Ref Expression
1 relogcl ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℝ$
2 1 recnd ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℂ$
3 efexp ${⊢}\left(\mathrm{log}{A}\in ℂ\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{N}\mathrm{log}{A}}={{\mathrm{e}}^{\mathrm{log}{A}}}^{{N}}$
4 2 3 sylan ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{N}\mathrm{log}{A}}={{\mathrm{e}}^{\mathrm{log}{A}}}^{{N}}$
5 reeflog ${⊢}{A}\in {ℝ}^{+}\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$
6 5 oveq1d ${⊢}{A}\in {ℝ}^{+}\to {{\mathrm{e}}^{\mathrm{log}{A}}}^{{N}}={{A}}^{{N}}$
7 6 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {{\mathrm{e}}^{\mathrm{log}{A}}}^{{N}}={{A}}^{{N}}$
8 4 7 eqtr2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {{A}}^{{N}}={\mathrm{e}}^{{N}\mathrm{log}{A}}$