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 \mathbb{Z}\right)\to A^N={\mathrm{e}}^{N\log A}$$

Proof

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