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 e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | negneg | |- ( N e. CC -> -u -u N = N ) |
|
| 2 | 1 | 3ad2ant2 | |- ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> -u -u N = N ) |
| 3 | 2 | oveq2d | |- ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ -u -u N ) = ( A ^ N ) ) |
| 4 | expneg | |- ( ( A e. CC /\ -u N e. NN0 ) -> ( A ^ -u -u N ) = ( 1 / ( A ^ -u N ) ) ) |
|
| 5 | 4 | 3adant2 | |- ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ -u -u N ) = ( 1 / ( A ^ -u N ) ) ) |
| 6 | 3 5 | eqtr3d | |- ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) ) |