Metamath Proof Explorer

Theorem m1exp1

Description: Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021)

Ref Expression
Assertion m1exp1 
|- ( N e. ZZ -> ( ( -u 1 ^ N ) = 1 <-> 2 || N ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 divides 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 || N <-> E. n e. ZZ ( n x. 2 ) = N ) )
3 1 2 mpan 
 |-  ( N e. ZZ -> ( 2 || N <-> E. n e. ZZ ( n x. 2 ) = N ) )
4 oveq2 
 |-  ( N = ( n x. 2 ) -> ( -u 1 ^ N ) = ( -u 1 ^ ( n x. 2 ) ) )
5 4 eqcoms 
 |-  ( ( n x. 2 ) = N -> ( -u 1 ^ N ) = ( -u 1 ^ ( n x. 2 ) ) )
6 zcn 
 |-  ( n e. ZZ -> n e. CC )
7 2cnd 
 |-  ( n e. ZZ -> 2 e. CC )
8 6 7 mulcomd 
 |-  ( n e. ZZ -> ( n x. 2 ) = ( 2 x. n ) )
9 8 oveq2d 
 |-  ( n e. ZZ -> ( -u 1 ^ ( n x. 2 ) ) = ( -u 1 ^ ( 2 x. n ) ) )
10 m1expeven 
 |-  ( n e. ZZ -> ( -u 1 ^ ( 2 x. n ) ) = 1 )
11 9 10 eqtrd 
 |-  ( n e. ZZ -> ( -u 1 ^ ( n x. 2 ) ) = 1 )
12 5 11 sylan9eqr 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = N ) -> ( -u 1 ^ N ) = 1 )
13 12 rexlimiva 
 |-  ( E. n e. ZZ ( n x. 2 ) = N -> ( -u 1 ^ N ) = 1 )
14 3 13 syl6bi 
 |-  ( N e. ZZ -> ( 2 || N -> ( -u 1 ^ N ) = 1 ) )
15 14 impcom 
 |-  ( ( 2 || N /\ N e. ZZ ) -> ( -u 1 ^ N ) = 1 )
16 simpl 
 |-  ( ( 2 || N /\ N e. ZZ ) -> 2 || N )
17 15 16 2thd 
 |-  ( ( 2 || N /\ N e. ZZ ) -> ( ( -u 1 ^ N ) = 1 <-> 2 || N ) )
18 ax-1ne0 
 |-  1 =/= 0
19 eqcom 
 |-  ( -u 1 = 1 <-> 1 = -u 1 )
20 ax-1cn 
 |-  1 e. CC
21 20 eqnegi 
 |-  ( 1 = -u 1 <-> 1 = 0 )
22 19 21 bitri 
 |-  ( -u 1 = 1 <-> 1 = 0 )
23 18 22 nemtbir 
 |-  -. -u 1 = 1
24 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
25 oveq2 
 |-  ( N = ( ( 2 x. n ) + 1 ) -> ( -u 1 ^ N ) = ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) )
26 25 eqcoms 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( -u 1 ^ N ) = ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) )
27 neg1cn 
 |-  -u 1 e. CC
28 27 a1i 
 |-  ( n e. ZZ -> -u 1 e. CC )
29 neg1ne0 
 |-  -u 1 =/= 0
30 29 a1i 
 |-  ( n e. ZZ -> -u 1 =/= 0 )
31 1 a1i 
 |-  ( n e. ZZ -> 2 e. ZZ )
32 id 
 |-  ( n e. ZZ -> n e. ZZ )
33 31 32 zmulcld 
 |-  ( n e. ZZ -> ( 2 x. n ) e. ZZ )
34 28 30 33 expp1zd 
 |-  ( n e. ZZ -> ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) = ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) )
35 10 oveq1d 
 |-  ( n e. ZZ -> ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) = ( 1 x. -u 1 ) )
36 27 mulid2i 
 |-  ( 1 x. -u 1 ) = -u 1
37 35 36 eqtrdi 
 |-  ( n e. ZZ -> ( ( -u 1 ^ ( 2 x. n ) ) x. -u 1 ) = -u 1 )
38 34 37 eqtrd 
 |-  ( n e. ZZ -> ( -u 1 ^ ( ( 2 x. n ) + 1 ) ) = -u 1 )
39 26 38 sylan9eqr 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = N ) -> ( -u 1 ^ N ) = -u 1 )
40 39 rexlimiva 
 |-  ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N -> ( -u 1 ^ N ) = -u 1 )
41 24 40 syl6bi 
 |-  ( N e. ZZ -> ( -. 2 || N -> ( -u 1 ^ N ) = -u 1 ) )
42 41 impcom 
 |-  ( ( -. 2 || N /\ N e. ZZ ) -> ( -u 1 ^ N ) = -u 1 )
43 42 eqeq1d 
 |-  ( ( -. 2 || N /\ N e. ZZ ) -> ( ( -u 1 ^ N ) = 1 <-> -u 1 = 1 ) )
44 23 43 mtbiri 
 |-  ( ( -. 2 || N /\ N e. ZZ ) -> -. ( -u 1 ^ N ) = 1 )
45 simpl 
 |-  ( ( -. 2 || N /\ N e. ZZ ) -> -. 2 || N )
46 44 45 2falsed 
 |-  ( ( -. 2 || N /\ N e. ZZ ) -> ( ( -u 1 ^ N ) = 1 <-> 2 || N ) )
47 17 46 pm2.61ian 
 |-  ( N e. ZZ -> ( ( -u 1 ^ N ) = 1 <-> 2 || N ) )