expneg

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		nnne0	$⊢ N \in ℕ \to N \neq 0$
3	2	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \neq 0$
4		nncn	$⊢ N \in ℕ \to N \in ℂ$
5	4	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℂ$
6	5	negeq0d	$⊢ (A \in ℂ \land N \in ℕ) \to (N = 0 \leftrightarrow - N = 0)$
7	6	necon3abid	$⊢ (A \in ℂ \land N \in ℕ) \to (N \neq 0 \leftrightarrow \neg - N = 0)$
8	3 7	mpbid	$⊢ (A \in ℂ \land N \in ℕ) \to \neg - N = 0$
9	8	iffalsed	$⊢ (A \in ℂ \land N \in ℕ) \to if (- N = 0, 1, if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)})) = if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)})$
10		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
11	10	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℕ_{0}$
12		nn0nlt0	$⊢ N \in ℕ_{0} \to \neg N < 0$
13	11 12	syl	$⊢ (A \in ℂ \land N \in ℕ) \to \neg N < 0$
14	11	nn0red	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℝ$
15	14	lt0neg1d	$⊢ (A \in ℂ \land N \in ℕ) \to (N < 0 \leftrightarrow 0 < - N)$
16	13 15	mtbid	$⊢ (A \in ℂ \land N \in ℕ) \to \neg 0 < - N$
17	16	iffalsed	$⊢ (A \in ℂ \land N \in ℕ) \to if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)}) = \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)}$
18	5	negnegd	$⊢ (A \in ℂ \land N \in ℕ) \to - -N = N$
19	18	fveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to seq 1 (\times (ℕ \times \{A\})) (- -N) = seq 1 (\times (ℕ \times \{A\})) (N)$
20	19	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)} = \frac{1}{seq 1 (\times (ℕ \times \{A\})) (N)}$
21	9 17 20	3eqtrd	$⊢ (A \in ℂ \land N \in ℕ) \to if (- N = 0, 1, if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)})) = \frac{1}{seq 1 (\times (ℕ \times \{A\})) (N)}$
22		nnnegz	$⊢ N \in ℕ \to - N \in ℤ$
23		expval	$⊢ (A \in ℂ \land - N \in ℤ) \to A^{- N} = if (- N = 0, 1, if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)}))$
24	22 23	sylan2	$⊢ (A \in ℂ \land N \in ℕ) \to A^{- N} = if (- N = 0, 1, if (0 < - N, seq 1 (\times (ℕ \times \{A\})) (- N), \frac{1}{seq 1 (\times (ℕ \times \{A\})) (- -N)}))$
25		expnnval	$⊢ (A \in ℂ \land N \in ℕ) \to A^{N} = seq 1 (\times (ℕ \times \{A\})) (N)$
26	25	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to \frac{1}{A^{N}} = \frac{1}{seq 1 (\times (ℕ \times \{A\})) (N)}$
27	21 24 26	3eqtr4d	$⊢ (A \in ℂ \land N \in ℕ) \to A^{- N} = \frac{1}{A^{N}}$
28		1div1e1	$⊢ \frac{1}{1} = 1$
29	28	eqcomi	$⊢ 1 = \frac{1}{1}$
30		negeq	$⊢ N = 0 \to - N = - 0$
31		neg0	$⊢ - 0 = 0$
32	30 31	eqtrdi	$⊢ N = 0 \to - N = 0$
33	32	oveq2d	$⊢ N = 0 \to A^{- N} = A^{0}$
34		exp0	$⊢ A \in ℂ \to A^{0} = 1$
35	33 34	sylan9eqr	$⊢ (A \in ℂ \land N = 0) \to A^{- N} = 1$
36		oveq2	$⊢ N = 0 \to A^{N} = A^{0}$
37	36 34	sylan9eqr	$⊢ (A \in ℂ \land N = 0) \to A^{N} = 1$
38	37	oveq2d	$⊢ (A \in ℂ \land N = 0) \to \frac{1}{A^{N}} = \frac{1}{1}$
39	29 35 38	3eqtr4a	$⊢ (A \in ℂ \land N = 0) \to A^{- N} = \frac{1}{A^{N}}$
40	27 39	jaodan	$⊢ (A \in ℂ \land (N \in ℕ \lor N = 0)) \to A^{- N} = \frac{1}{A^{N}}$
41	1 40	sylan2b	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{- N} = \frac{1}{A^{N}}$

Metamath Proof Explorer

Theorem expneg

Proof