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