Metamath Proof Explorer

Theorem oexpnegnz

Description: The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020)

Ref Expression
Assertion oexpnegnz 
|- ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( N e. Odd -> N e. ZZ )
2 odd2np1ALTV 
 |-  ( N e. ZZ -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
3 1 2 syl 
 |-  ( N e. Odd -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
4 3 biimpd 
 |-  ( N e. Odd -> ( N e. Odd -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
5 4 pm2.43i 
 |-  ( N e. Odd -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N )
6 5 3ad2ant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N )
7 simpl1 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> A e. CC )
8 simpl2 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> A =/= 0 )
9 2z 
 |-  2 e. ZZ
10 simprl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> n e. ZZ )
11 zmulcl 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
12 9 10 11 sylancr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( 2 x. n ) e. ZZ )
13 7 8 12 expclzd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( 2 x. n ) ) e. CC )
14 13 7 mulneg2d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A ^ ( 2 x. n ) ) x. -u A ) = -u ( ( A ^ ( 2 x. n ) ) x. A ) )
15 sqneg 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
16 7 15 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ 2 ) = ( A ^ 2 ) )
17 16 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A ^ 2 ) ^ n ) = ( ( A ^ 2 ) ^ n ) )
18 7 negcld 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u A e. CC )
19 7 8 negne0d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u A =/= 0 )
20 9 a1i 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) -> 2 e. ZZ )
21 simpl 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) -> n e. ZZ )
22 20 21 jca 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) -> ( 2 e. ZZ /\ n e. ZZ ) )
23 22 adantl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( 2 e. ZZ /\ n e. ZZ ) )
24 18 19 23 jca31 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A e. CC /\ -u A =/= 0 ) /\ ( 2 e. ZZ /\ n e. ZZ ) ) )
25 expmulz 
 |-  ( ( ( -u A e. CC /\ -u A =/= 0 ) /\ ( 2 e. ZZ /\ n e. ZZ ) ) -> ( -u A ^ ( 2 x. n ) ) = ( ( -u A ^ 2 ) ^ n ) )
26 24 25 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( 2 x. n ) ) = ( ( -u A ^ 2 ) ^ n ) )
27 7 8 23 jca31 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A e. CC /\ A =/= 0 ) /\ ( 2 e. ZZ /\ n e. ZZ ) ) )
28 expmulz 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( 2 e. ZZ /\ n e. ZZ ) ) -> ( A ^ ( 2 x. n ) ) = ( ( A ^ 2 ) ^ n ) )
29 27 28 syl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( 2 x. n ) ) = ( ( A ^ 2 ) ^ n ) )
30 17 26 29 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( 2 x. n ) ) = ( A ^ ( 2 x. n ) ) )
31 30 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A ^ ( 2 x. n ) ) x. -u A ) = ( ( A ^ ( 2 x. n ) ) x. -u A ) )
32 18 19 12 expp1zd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( ( 2 x. n ) + 1 ) ) = ( ( -u A ^ ( 2 x. n ) ) x. -u A ) )
33 simprr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( 2 x. n ) + 1 ) = N )
34 33 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( ( 2 x. n ) + 1 ) ) = ( -u A ^ N ) )
35 32 34 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A ^ ( 2 x. n ) ) x. -u A ) = ( -u A ^ N ) )
36 31 35 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A ^ ( 2 x. n ) ) x. -u A ) = ( -u A ^ N ) )
37 14 36 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u ( ( A ^ ( 2 x. n ) ) x. A ) = ( -u A ^ N ) )
38 7 8 12 expp1zd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( ( 2 x. n ) + 1 ) ) = ( ( A ^ ( 2 x. n ) ) x. A ) )
39 33 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( ( 2 x. n ) + 1 ) ) = ( A ^ N ) )
40 38 39 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A ^ ( 2 x. n ) ) x. A ) = ( A ^ N ) )
41 40 negeqd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u ( ( A ^ ( 2 x. n ) ) x. A ) = -u ( A ^ N ) )
42 37 41 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ N ) = -u ( A ^ N ) )
43 6 42 rexlimddv 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )