expnegz

Description: Value of a nonzero complex number raised to the negative of an integer power. (Contributed by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expnegz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{- N} = \frac{1}{A^{N}}$

Proof

Step	Hyp	Ref	Expression
1		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
2		expneg	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{- N} = \frac{1}{A^{N}}$
3	2	ex	$⊢ A \in ℂ \to (N \in ℕ_{0} \to A^{- N} = \frac{1}{A^{N}})$
4	3	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℝ) \to (N \in ℕ_{0} \to A^{- N} = \frac{1}{A^{N}})$
5		simpll	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A \in ℂ$
6		simprl	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to N \in ℝ$
7	6	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to N \in ℂ$
8		simprr	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to - N \in ℕ_{0}$
9		expneg2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$
10	5 7 8 9	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A^{N} = \frac{1}{A^{- N}}$
11	10	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to \frac{1}{A^{N}} = \frac{1}{\frac{1}{A^{- N}}}$
12		expcl	$⊢ (A \in ℂ \land - N \in ℕ_{0}) \to A^{- N} \in ℂ$
13	12	ad2ant2rl	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A^{- N} \in ℂ$
14		simplr	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A \neq 0$
15	8	nn0zd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to - N \in ℤ$
16		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - N \in ℤ) \to A^{- N} \neq 0$
17	5 14 15 16	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A^{- N} \neq 0$
18	13 17	recrecd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to \frac{1}{\frac{1}{A^{- N}}} = A^{- N}$
19	11 18	eqtr2d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ_{0})) \to A^{- N} = \frac{1}{A^{N}}$
20	19	expr	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℝ) \to (- N \in ℕ_{0} \to A^{- N} = \frac{1}{A^{N}})$
21	4 20	jaod	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℝ) \to ((N \in ℕ_{0} \lor - N \in ℕ_{0}) \to A^{- N} = \frac{1}{A^{N}})$
22	21	expimpd	$⊢ (A \in ℂ \land A \neq 0) \to ((N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to A^{- N} = \frac{1}{A^{N}})$
23	1 22	biimtrid	$⊢ (A \in ℂ \land A \neq 0) \to (N \in ℤ \to A^{- N} = \frac{1}{A^{N}})$
24	23	3impia	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{- N} = \frac{1}{A^{N}}$

Metamath Proof Explorer

Theorem expnegz

Proof