Theorem explog

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

	Ref	Expression
Assertion	explog	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N={\mathrm{e}}^{N\log A}$$

Proof

Step	Hyp	Ref	Expression
1		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
2		efexp	$$⊢\left(\log A\in ℂ\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{N\log A}={{\mathrm{e}}^{\log A}}^N$$
3	1 2	stoic3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{N\log A}={{\mathrm{e}}^{\log A}}^N$$
4		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
5	4	3adant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to {\mathrm{e}}^{\log A}=A$$
6	5	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to {{\mathrm{e}}^{\log A}}^N=A^N$$
7	3 6	eqtr2d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N={\mathrm{e}}^{N\log A}$$