Metamath Proof Explorer


Theorem expnegd

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

Ref Expression
Hypotheses expcld.1 φA
sqrecd.1 φA0
expclzd.3 φN
Assertion expnegd φAN=1AN

Proof

Step Hyp Ref Expression
1 expcld.1 φA
2 sqrecd.1 φA0
3 expclzd.3 φN
4 expnegz AA0NAN=1AN
5 1 2 3 4 syl3anc φAN=1AN