Metamath Proof Explorer


Theorem expneg2

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 expneg2 A N N 0 A N = 1 A N

Proof

Step Hyp Ref Expression
1 negneg N -N = N
2 1 3ad2ant2 A N N 0 -N = N
3 2 oveq2d A N N 0 A -N = A N
4 expneg A N 0 A -N = 1 A N
5 4 3adant2 A N N 0 A -N = 1 A N
6 3 5 eqtr3d A N N 0 A N = 1 A N