Theorem expneg2

Description: Value of a complex number raised to a nonpositive integer power. When A = 0 and N is nonzero, both sides have the "value" ( 1 / 0 ) ; relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expneg2	$$⊢\left(A\in ℂ\wedge N\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to A^N=\frac{1}{A^{-N}}$$

Proof

Step	Hyp	Ref	Expression
1		negneg	$$⊢N\in ℂ\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=N$$
2	1	3ad2ant2	$$⊢\left(A\in ℂ\wedge N\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=N$$
3	2	oveq2d	$$⊢\left(A\in ℂ\wedge N\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to A^{-\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}}=A^N$$
4		expneg	$$⊢\left(A\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to A^{-\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}}=\frac{1}{A^{-N}}$$
5	4	3adant2	$$⊢\left(A\in ℂ\wedge N\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to A^{-\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}}=\frac{1}{A^{-N}}$$
6	3 5	eqtr3d	$$⊢\left(A\in ℂ\wedge N\in ℂ\wedge -N\in {\mathbb{N}}_0\right)\to A^N=\frac{1}{A^{-N}}$$