Metamath Proof Explorer

Theorem m1expoddALTV

Description: Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020)

Ref Expression
Assertion m1expoddALTV 
|- ( N e. Odd -> ( -u 1 ^ N ) = -u 1 )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( N e. Odd -> N e. ZZ )
2 1 zcnd 
 |-  ( N e. Odd -> N e. CC )
3 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
4 3 eqcomd 
 |-  ( N e. CC -> N = ( ( N - 1 ) + 1 ) )
5 2 4 syl 
 |-  ( N e. Odd -> N = ( ( N - 1 ) + 1 ) )
6 5 oveq2d 
 |-  ( N e. Odd -> ( -u 1 ^ N ) = ( -u 1 ^ ( ( N - 1 ) + 1 ) ) )
7 neg1cn 
 |-  -u 1 e. CC
8 7 a1i 
 |-  ( N e. Odd -> -u 1 e. CC )
9 neg1ne0 
 |-  -u 1 =/= 0
10 9 a1i 
 |-  ( N e. Odd -> -u 1 =/= 0 )
11 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
12 1 11 syl 
 |-  ( N e. Odd -> ( N - 1 ) e. ZZ )
13 8 10 12 expp1zd 
 |-  ( N e. Odd -> ( -u 1 ^ ( ( N - 1 ) + 1 ) ) = ( ( -u 1 ^ ( N - 1 ) ) x. -u 1 ) )
14 oddm1eveni 
 |-  ( N e. Odd -> ( N - 1 ) e. Even )
15 m1expevenALTV 
 |-  ( ( N - 1 ) e. Even -> ( -u 1 ^ ( N - 1 ) ) = 1 )
16 14 15 syl 
 |-  ( N e. Odd -> ( -u 1 ^ ( N - 1 ) ) = 1 )
17 16 oveq1d 
 |-  ( N e. Odd -> ( ( -u 1 ^ ( N - 1 ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
18 8 mulid2d 
 |-  ( N e. Odd -> ( 1 x. -u 1 ) = -u 1 )
19 17 18 eqtrd 
 |-  ( N e. Odd -> ( ( -u 1 ^ ( N - 1 ) ) x. -u 1 ) = -u 1 )
20 6 13 19 3eqtrd 
 |-  ( N e. Odd -> ( -u 1 ^ N ) = -u 1 )