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	syl5eq	|- ( 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 )