Metamath Proof Explorer

Theorem m1expeven

Description: Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 1 2timesd 
 |-  ( N e. ZZ -> ( 2 x. N ) = ( N + N ) )
3 2 oveq2d 
 |-  ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = ( -u 1 ^ ( N + N ) ) )
4 neg1cn 
 |-  -u 1 e. CC
5 neg1ne0 
 |-  -u 1 =/= 0
6 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( N e. ZZ /\ N e. ZZ ) ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
7 4 5 6 mpanl12 
 |-  ( ( N e. ZZ /\ N e. ZZ ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
8 7 anidms 
 |-  ( N e. ZZ -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
9 m1expcl2 
 |-  ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
10 ovex 
 |-  ( -u 1 ^ N ) e. _V
11 10 elpr 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } <-> ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) )
12 oveq12 
 |-  ( ( ( -u 1 ^ N ) = -u 1 /\ ( -u 1 ^ N ) = -u 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( -u 1 x. -u 1 ) )
13 12 anidms 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( -u 1 x. -u 1 ) )
14 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
15 13 14 eqtrdi 
 |-  ( ( -u 1 ^ N ) = -u 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
16 oveq12 
 |-  ( ( ( -u 1 ^ N ) = 1 /\ ( -u 1 ^ N ) = 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( 1 x. 1 ) )
17 16 anidms 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = ( 1 x. 1 ) )
18 1t1e1 
 |-  ( 1 x. 1 ) = 1
19 17 18 eqtrdi 
 |-  ( ( -u 1 ^ N ) = 1 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
20 15 19 jaoi 
 |-  ( ( ( -u 1 ^ N ) = -u 1 \/ ( -u 1 ^ N ) = 1 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
21 11 20 sylbi 
 |-  ( ( -u 1 ^ N ) e. { -u 1 , 1 } -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
22 9 21 syl 
 |-  ( N e. ZZ -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
23 3 8 22 3eqtrd 
 |-  ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 )