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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elznn0 | |
|
2 | expneg | |
|
3 | 2 | ex | |
4 | 3 | ad2antrr | |
5 | simpll | |
|
6 | simprl | |
|
7 | 6 | recnd | |
8 | simprr | |
|
9 | expneg2 | |
|
10 | 5 7 8 9 | syl3anc | |
11 | 10 | oveq2d | |
12 | expcl | |
|
13 | 12 | ad2ant2rl | |
14 | simplr | |
|
15 | 8 | nn0zd | |
16 | expne0i | |
|
17 | 5 14 15 16 | syl3anc | |
18 | 13 17 | recrecd | |
19 | 11 18 | eqtr2d | |
20 | 19 | expr | |
21 | 4 20 | jaod | |
22 | 21 | expimpd | |
23 | 1 22 | biimtrid | |
24 | 23 | 3impia | |