reexplog

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

		Ref	Expression
	Assertion	reexplog	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to A^{N} = e^{N \log A}$

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

Metamath Proof Explorer