Metamath Proof Explorer

Theorem oexpnegALTV

Description: The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015) (Revised by AV, 19-Jun-2020) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion oexpnegALTV 
|- ( ( A e. CC /\ N e. NN /\ 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 ibi 
 |-  ( N e. Odd -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N )
5 4 3ad2ant3 
 |-  ( ( A e. CC /\ N e. NN /\ N e. Odd ) -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N )
6 simpl1 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> A e. CC )
7 simprr 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( 2 x. n ) + 1 ) = N )
8 simpl2 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> N e. NN )
9 8 nncnd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> N e. CC )
10 1cnd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> 1 e. CC )
11 2z 
 |-  2 e. ZZ
12 simprl 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> n e. ZZ )
13 zmulcl 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
14 11 12 13 sylancr 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( 2 x. n ) e. ZZ )
15 14 zcnd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( 2 x. n ) e. CC )
16 9 10 15 subadd2d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( N - 1 ) = ( 2 x. n ) <-> ( ( 2 x. n ) + 1 ) = N ) )
17 7 16 mpbird 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( N - 1 ) = ( 2 x. n ) )
18 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
19 8 18 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( N - 1 ) e. NN0 )
20 17 19 eqeltrrd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( 2 x. n ) e. NN0 )
21 6 20 expcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( 2 x. n ) ) e. CC )
22 21 6 mulneg2d 
 |-  ( ( ( A e. CC /\ N e. NN /\ 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 ) )
23 sqneg 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
24 6 23 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ 2 ) = ( A ^ 2 ) )
25 24 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A ^ 2 ) ^ n ) = ( ( A ^ 2 ) ^ n ) )
26 6 negcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u A e. CC )
27 2rp 
 |-  2 e. RR+
28 27 a1i 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> 2 e. RR+ )
29 12 zred 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> n e. RR )
30 20 nn0ge0d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> 0 <_ ( 2 x. n ) )
31 28 29 30 prodge0rd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> 0 <_ n )
32 elnn0z 
 |-  ( n e. NN0 <-> ( n e. ZZ /\ 0 <_ n ) )
33 12 31 32 sylanbrc 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> n e. NN0 )
34 2nn0 
 |-  2 e. NN0
35 34 a1i 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> 2 e. NN0 )
36 26 33 35 expmuld 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( 2 x. n ) ) = ( ( -u A ^ 2 ) ^ n ) )
37 6 33 35 expmuld 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( 2 x. n ) ) = ( ( A ^ 2 ) ^ n ) )
38 25 36 37 3eqtr4d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( 2 x. n ) ) = ( A ^ ( 2 x. n ) ) )
39 38 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ 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 ) )
40 26 20 expp1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ 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 ) )
41 7 oveq2d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ ( ( 2 x. n ) + 1 ) ) = ( -u A ^ N ) )
42 40 41 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( -u A ^ ( 2 x. n ) ) x. -u A ) = ( -u A ^ N ) )
43 39 42 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A ^ ( 2 x. n ) ) x. -u A ) = ( -u A ^ N ) )
44 22 43 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u ( ( A ^ ( 2 x. n ) ) x. A ) = ( -u A ^ N ) )
45 6 20 expp1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( ( 2 x. n ) + 1 ) ) = ( ( A ^ ( 2 x. n ) ) x. A ) )
46 7 oveq2d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( A ^ ( ( 2 x. n ) + 1 ) ) = ( A ^ N ) )
47 45 46 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( ( A ^ ( 2 x. n ) ) x. A ) = ( A ^ N ) )
48 47 negeqd 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> -u ( ( A ^ ( 2 x. n ) ) x. A ) = -u ( A ^ N ) )
49 44 48 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ N e. Odd ) /\ ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) ) -> ( -u A ^ N ) = -u ( A ^ N ) )
50 5 49 rexlimddv 
 |-  ( ( A e. CC /\ N e. NN /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )