Metamath Proof Explorer


Theorem expn1

Description: A complex number raised to the negative one power is its reciprocal. When A = 0 , 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 expn1
|- ( A e. CC -> ( A ^ -u 1 ) = ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 1nn0
 |-  1 e. NN0
2 expneg
 |-  ( ( A e. CC /\ 1 e. NN0 ) -> ( A ^ -u 1 ) = ( 1 / ( A ^ 1 ) ) )
3 1 2 mpan2
 |-  ( A e. CC -> ( A ^ -u 1 ) = ( 1 / ( A ^ 1 ) ) )
4 exp1
 |-  ( A e. CC -> ( A ^ 1 ) = A )
5 4 oveq2d
 |-  ( A e. CC -> ( 1 / ( A ^ 1 ) ) = ( 1 / A ) )
6 3 5 eqtrd
 |-  ( A e. CC -> ( A ^ -u 1 ) = ( 1 / A ) )