Theorem expneg2

Description: Value of a complex number raised to a negative integer power. (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 ) ) )

Proof

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 ) ) )