Metamath Proof Explorer


Theorem expneg

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

Ref Expression
Assertion expneg
|- ( ( A e. CC /\ N e. NN0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 elnn0
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 nnne0
 |-  ( N e. NN -> N =/= 0 )
3 2 adantl
 |-  ( ( A e. CC /\ N e. NN ) -> N =/= 0 )
4 nncn
 |-  ( N e. NN -> N e. CC )
5 4 adantl
 |-  ( ( A e. CC /\ N e. NN ) -> N e. CC )
6 5 negeq0d
 |-  ( ( A e. CC /\ N e. NN ) -> ( N = 0 <-> -u N = 0 ) )
7 6 necon3abid
 |-  ( ( A e. CC /\ N e. NN ) -> ( N =/= 0 <-> -. -u N = 0 ) )
8 3 7 mpbid
 |-  ( ( A e. CC /\ N e. NN ) -> -. -u N = 0 )
9 8 iffalsed
 |-  ( ( A e. CC /\ N e. NN ) -> if ( -u N = 0 , 1 , if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) ) = if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) )
10 nnnn0
 |-  ( N e. NN -> N e. NN0 )
11 10 adantl
 |-  ( ( A e. CC /\ N e. NN ) -> N e. NN0 )
12 nn0nlt0
 |-  ( N e. NN0 -> -. N < 0 )
13 11 12 syl
 |-  ( ( A e. CC /\ N e. NN ) -> -. N < 0 )
14 11 nn0red
 |-  ( ( A e. CC /\ N e. NN ) -> N e. RR )
15 14 lt0neg1d
 |-  ( ( A e. CC /\ N e. NN ) -> ( N < 0 <-> 0 < -u N ) )
16 13 15 mtbid
 |-  ( ( A e. CC /\ N e. NN ) -> -. 0 < -u N )
17 16 iffalsed
 |-  ( ( A e. CC /\ N e. NN ) -> if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) = ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) )
18 5 negnegd
 |-  ( ( A e. CC /\ N e. NN ) -> -u -u N = N )
19 18 fveq2d
 |-  ( ( A e. CC /\ N e. NN ) -> ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
20 19 oveq2d
 |-  ( ( A e. CC /\ N e. NN ) -> ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) = ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) ) )
21 9 17 20 3eqtrd
 |-  ( ( A e. CC /\ N e. NN ) -> if ( -u N = 0 , 1 , if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) ) = ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) ) )
22 nnnegz
 |-  ( N e. NN -> -u N e. ZZ )
23 expval
 |-  ( ( A e. CC /\ -u N e. ZZ ) -> ( A ^ -u N ) = if ( -u N = 0 , 1 , if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) ) )
24 22 23 sylan2
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ -u N ) = if ( -u N = 0 , 1 , if ( 0 < -u N , ( seq 1 ( x. , ( NN X. { A } ) ) ` -u N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` -u -u N ) ) ) ) )
25 expnnval
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
26 25 oveq2d
 |-  ( ( A e. CC /\ N e. NN ) -> ( 1 / ( A ^ N ) ) = ( 1 / ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) ) )
27 21 24 26 3eqtr4d
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
28 1div1e1
 |-  ( 1 / 1 ) = 1
29 28 eqcomi
 |-  1 = ( 1 / 1 )
30 negeq
 |-  ( N = 0 -> -u N = -u 0 )
31 neg0
 |-  -u 0 = 0
32 30 31 eqtrdi
 |-  ( N = 0 -> -u N = 0 )
33 32 oveq2d
 |-  ( N = 0 -> ( A ^ -u N ) = ( A ^ 0 ) )
34 exp0
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
35 33 34 sylan9eqr
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ -u N ) = 1 )
36 oveq2
 |-  ( N = 0 -> ( A ^ N ) = ( A ^ 0 ) )
37 36 34 sylan9eqr
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ N ) = 1 )
38 37 oveq2d
 |-  ( ( A e. CC /\ N = 0 ) -> ( 1 / ( A ^ N ) ) = ( 1 / 1 ) )
39 29 35 38 3eqtr4a
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
40 27 39 jaodan
 |-  ( ( A e. CC /\ ( N e. NN \/ N = 0 ) ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
41 1 40 sylan2b
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )