Metamath Proof Explorer

Theorem expneg

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