Metamath Proof Explorer

Theorem expnegz

Description: Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expnegz 
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
2 expneg 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
3 2 ex 
 |-  ( A e. CC -> ( N e. NN0 -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
4 3 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. RR ) -> ( N e. NN0 -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
5 simpll 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> A e. CC )
6 simprl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> N e. RR )
7 6 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> N e. CC )
8 simprr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> -u N e. NN0 )
9 expneg2 
 |-  ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
10 5 7 8 9 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
11 10 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( 1 / ( A ^ N ) ) = ( 1 / ( 1 / ( A ^ -u N ) ) ) )
12 expcl 
 |-  ( ( A e. CC /\ -u N e. NN0 ) -> ( A ^ -u N ) e. CC )
13 12 ad2ant2rl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( A ^ -u N ) e. CC )
14 simplr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> A =/= 0 )
15 8 nn0zd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> -u N e. ZZ )
16 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u N e. ZZ ) -> ( A ^ -u N ) =/= 0 )
17 5 14 15 16 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( A ^ -u N ) =/= 0 )
18 13 17 recrecd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( 1 / ( 1 / ( A ^ -u N ) ) ) = ( A ^ -u N ) )
19 11 18 eqtr2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. RR /\ -u N e. NN0 ) ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
20 19 expr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. RR ) -> ( -u N e. NN0 -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
21 4 20 jaod 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ N e. RR ) -> ( ( N e. NN0 \/ -u N e. NN0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
22 21 expimpd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
23 1 22 syl5bi 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( N e. ZZ -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) ) )
24 23 3impia 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )