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	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$

Proof

Step	Hyp	Ref	Expression
1		negneg	$⊢ N \in ℂ \to - -N = N$
2	1	3ad2ant2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to - -N = N$
3	2	oveq2d	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{- -N} = A^{N}$
4		expneg	$⊢ (A \in ℂ \land - N \in ℕ_{0}) \to A^{- -N} = \frac{1}{A^{- N}}$
5	4	3adant2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{- -N} = \frac{1}{A^{- N}}$
6	3 5	eqtr3d	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$

Metamath Proof Explorer

Theorem expneg2

Proof