# Metamath Proof Explorer

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

### Proof

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