# Metamath Proof Explorer

## Theorem expneg

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

Ref Expression
Assertion expneg ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{-{N}}=\frac{1}{{{A}}^{{N}}}$

### Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
2 nnne0 ${⊢}{N}\in ℕ\to {N}\ne 0$
3 2 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {N}\ne 0$
4 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
5 4 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {N}\in ℂ$
6 5 negeq0d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \left({N}=0↔-{N}=0\right)$
7 6 necon3abid ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \left({N}\ne 0↔¬-{N}=0\right)$
8 3 7 mpbid ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to ¬-{N}=0$
9 8 iffalsed ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to if\left(-{N}=0,1,if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)\right)=if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)$
10 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
11 10 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {N}\in {ℕ}_{0}$
12 nn0nlt0 ${⊢}{N}\in {ℕ}_{0}\to ¬{N}<0$
13 11 12 syl ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to ¬{N}<0$
14 11 nn0red ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {N}\in ℝ$
15 14 lt0neg1d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \left({N}<0↔0<-{N}\right)$
16 13 15 mtbid ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to ¬0<-{N}$
17 16 iffalsed ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)=\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}$
18 5 negnegd ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to --{N}={N}$
19 18 fveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)$
20 19 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}=\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)}$
21 9 17 20 3eqtrd ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to if\left(-{N}=0,1,if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)\right)=\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)}$
22 nnnegz ${⊢}{N}\in ℕ\to -{N}\in ℤ$
23 expval ${⊢}\left({A}\in ℂ\wedge -{N}\in ℤ\right)\to {{A}}^{-{N}}=if\left(-{N}=0,1,if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)\right)$
24 22 23 sylan2 ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{-{N}}=if\left(-{N}=0,1,if\left(0<-{N},seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(-{N}\right),\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left(--{N}\right)}\right)\right)$
25 expnnval ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{{N}}=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)$
26 25 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \frac{1}{{{A}}^{{N}}}=\frac{1}{seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)}$
27 21 24 26 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\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 syl6eq ${⊢}{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 ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{-{N}}=1$
36 oveq2 ${⊢}{N}=0\to {{A}}^{{N}}={{A}}^{0}$
37 36 34 sylan9eqr ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{{N}}=1$
38 37 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to \frac{1}{{{A}}^{{N}}}=\frac{1}{1}$
39 29 35 38 3eqtr4a ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{-{N}}=\frac{1}{{{A}}^{{N}}}$
40 27 39 jaodan ${⊢}\left({A}\in ℂ\wedge \left({N}\in ℕ\vee {N}=0\right)\right)\to {{A}}^{-{N}}=\frac{1}{{{A}}^{{N}}}$
41 1 40 sylan2b ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{-{N}}=\frac{1}{{{A}}^{{N}}}$