explog

Description: Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008)

		Ref	Expression
	Assertion	explog	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} = e^{N \log A}$

Step	Hyp	Ref	Expression
1		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
2		efexp	$⊢ (\log A \in ℂ \land N \in ℤ) \to e^{N \log A} = {e^{\log A}}^{N}$
3	1 2	stoic3	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to e^{N \log A} = {e^{\log A}}^{N}$
4		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
5	4	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to e^{\log A} = A$
6	5	oveq1d	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {e^{\log A}}^{N} = A^{N}$
7	3 6	eqtr2d	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} = e^{N \log A}$

Metamath Proof Explorer