This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem m1expevenALTV

Description: Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 6-Jul-2020)

Ref Expression
Assertion m1expevenALTV 
|- ( N e. Even -> ( -u 1 ^ N ) = 1 )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( n = N -> ( n = ( 2 x. i ) <-> N = ( 2 x. i ) ) )
2 1 rexbidv 
 |-  ( n = N -> ( E. i e. ZZ n = ( 2 x. i ) <-> E. i e. ZZ N = ( 2 x. i ) ) )
3 dfeven4 
 |-  Even = { n e. ZZ | E. i e. ZZ n = ( 2 x. i ) }
4 2 3 elrab2 
 |-  ( N e. Even <-> ( N e. ZZ /\ E. i e. ZZ N = ( 2 x. i ) ) )
5 oveq2 
 |-  ( N = ( 2 x. i ) -> ( -u 1 ^ N ) = ( -u 1 ^ ( 2 x. i ) ) )
6 neg1cn 
 |-  -u 1 e. CC
7 6 a1i 
 |-  ( i e. ZZ -> -u 1 e. CC )
8 neg1ne0 
 |-  -u 1 =/= 0
9 8 a1i 
 |-  ( i e. ZZ -> -u 1 =/= 0 )
10 2z 
 |-  2 e. ZZ
11 10 a1i 
 |-  ( i e. ZZ -> 2 e. ZZ )
12 id 
 |-  ( i e. ZZ -> i e. ZZ )
13 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ i e. ZZ ) ) -> ( -u 1 ^ ( 2 x. i ) ) = ( ( -u 1 ^ 2 ) ^ i ) )
14 7 9 11 12 13 syl22anc 
 |-  ( i e. ZZ -> ( -u 1 ^ ( 2 x. i ) ) = ( ( -u 1 ^ 2 ) ^ i ) )
15 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
16 15 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ i ) = ( 1 ^ i )
17 1exp 
 |-  ( i e. ZZ -> ( 1 ^ i ) = 1 )
18 16 17 eqtrid 
 |-  ( i e. ZZ -> ( ( -u 1 ^ 2 ) ^ i ) = 1 )
19 14 18 eqtrd 
 |-  ( i e. ZZ -> ( -u 1 ^ ( 2 x. i ) ) = 1 )
20 19 adantl 
 |-  ( ( N e. ZZ /\ i e. ZZ ) -> ( -u 1 ^ ( 2 x. i ) ) = 1 )
21 5 20 sylan9eqr 
 |-  ( ( ( N e. ZZ /\ i e. ZZ ) /\ N = ( 2 x. i ) ) -> ( -u 1 ^ N ) = 1 )
22 21 rexlimdva2 
 |-  ( N e. ZZ -> ( E. i e. ZZ N = ( 2 x. i ) -> ( -u 1 ^ N ) = 1 ) )
23 22 imp 
 |-  ( ( N e. ZZ /\ E. i e. ZZ N = ( 2 x. i ) ) -> ( -u 1 ^ N ) = 1 )
24 4 23 sylbi 
 |-  ( N e. Even -> ( -u 1 ^ N ) = 1 )