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 )