# 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 ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \mathrm{log}{{A}}^{{N}}={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 eqtrd ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{N}\mathrm{log}{A}}={{A}}^{{N}}$
9 8 fveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \mathrm{log}{\mathrm{e}}^{{N}\mathrm{log}{A}}=\mathrm{log}{{A}}^{{N}}$
10 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
11 remulcl ${⊢}\left({N}\in ℝ\wedge \mathrm{log}{A}\in ℝ\right)\to {N}\mathrm{log}{A}\in ℝ$
12 10 1 11 syl2anr ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {N}\mathrm{log}{A}\in ℝ$
13 relogef ${⊢}{N}\mathrm{log}{A}\in ℝ\to \mathrm{log}{\mathrm{e}}^{{N}\mathrm{log}{A}}={N}\mathrm{log}{A}$
14 12 13 syl ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \mathrm{log}{\mathrm{e}}^{{N}\mathrm{log}{A}}={N}\mathrm{log}{A}$
15 9 14 eqtr3d ${⊢}\left({A}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \mathrm{log}{{A}}^{{N}}={N}\mathrm{log}{A}$