Metamath Proof Explorer

Theorem m1expo

Description: Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021)

Ref Expression
Assertion m1expo 
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( -u 1 ^ N ) = -u 1 )

Proof

Step Hyp Ref Expression
1 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
2 oveq2 
 |-  ( N = ( ( 2 x. n ) + 1 ) -> ( -u 1 ^ N ) = ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) )
3 2 eqcoms 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( -u 1 ^ N ) = ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) )
4 neg1cn 
 |-  -u 1 e. CC
5 4 a1i 
 |-  ( n e. ZZ -> -u 1 e. CC )
6 neg1ne0 
 |-  -u 1 =/= 0
7 6 a1i 
 |-  ( n e. ZZ -> -u 1 =/= 0 )
8 2z 
 |-  2 e. ZZ
9 8 a1i 
 |-  ( n e. ZZ -> 2 e. ZZ )
10 id 
 |-  ( n e. ZZ -> n e. ZZ )
11 9 10 zmulcld 
 |-  ( n e. ZZ -> ( 2 x. n ) e. ZZ )
12 5 7 11 expp1zd 
 |-  ( n e. ZZ -> ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) = ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) )
13 m1expeven 
 |-  ( n e. ZZ -> ( -u 1 ^ ( 2 x. n ) ) = 1 )
14 13 oveq1d 
 |-  ( n e. ZZ -> ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
15 4 mulid2i 
 |-  ( 1 x. -u 1 ) = -u 1
16 14 15 eqtrdi 
 |-  ( n e. ZZ -> ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) = -u 1 )
17 12 16 eqtrd 
 |-  ( n e. ZZ -> ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) = -u 1 )
18 17 adantl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) = -u 1 )
19 3 18 sylan9eqr 
 |-  ( ( ( N e. ZZ /\ n e. ZZ ) /\ ( ( 2 x. n ) + 1 ) = N ) -> ( -u 1 ^ N ) = -u 1 )
20 19 rexlimdva2 
 |-  ( N e. ZZ -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N -> ( -u 1 ^ N ) = -u 1 ) )
21 1 20 sylbid 
 |-  ( N e. ZZ -> ( -. 2 || N -> ( -u 1 ^ N ) = -u 1 ) )
22 21 imp 
 |-  ( ( N e. ZZ /\ -. 2 || N ) -> ( -u 1 ^ N ) = -u 1 )