Metamath Proof Explorer


Theorem 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 AA0NAN=1AN

Proof

Step Hyp Ref Expression
1 elznn0 NNN0N0
2 expneg AN0AN=1AN
3 2 ex AN0AN=1AN
4 3 ad2antrr AA0NN0AN=1AN
5 simpll AA0NN0A
6 simprl AA0NN0N
7 6 recnd AA0NN0N
8 simprr AA0NN0N0
9 expneg2 ANN0AN=1AN
10 5 7 8 9 syl3anc AA0NN0AN=1AN
11 10 oveq2d AA0NN01AN=11AN
12 expcl AN0AN
13 12 ad2ant2rl AA0NN0AN
14 simplr AA0NN0A0
15 8 nn0zd AA0NN0N
16 expne0i AA0NAN0
17 5 14 15 16 syl3anc AA0NN0AN0
18 13 17 recrecd AA0NN011AN=AN
19 11 18 eqtr2d AA0NN0AN=1AN
20 19 expr AA0NN0AN=1AN
21 4 20 jaod AA0NN0N0AN=1AN
22 21 expimpd AA0NN0N0AN=1AN
23 1 22 biimtrid AA0NAN=1AN
24 23 3impia AA0NAN=1AN