Theorem m1expe

Description: Exponentiation of -1 by an even power. Variant of m1expeven . (Contributed by AV, 25-Jun-2021)

	Ref	Expression
Assertion	m1expe	|- ( 2 || N -> ( -u 1 ^ N ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		even2n	|- ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )
2		oveq2	|- ( N = ( 2 x. n ) -> ( -u 1 ^ N ) = ( -u 1 ^ ( 2 x. n ) ) )
3	2	eqcoms	|- ( ( 2 x. n ) = N -> ( -u 1 ^ N ) = ( -u 1 ^ ( 2 x. n ) ) )
4		m1expeven	|- ( n e. ZZ -> ( -u 1 ^ ( 2 x. n ) ) = 1 )
5	3 4	sylan9eqr	|- ( ( n e. ZZ /\ ( 2 x. n ) = N ) -> ( -u 1 ^ N ) = 1 )
6	5	rexlimiva	|- ( E. n e. ZZ ( 2 x. n ) = N -> ( -u 1 ^ N ) = 1 )
7	1 6	sylbi	|- ( 2 || N -> ( -u 1 ^ N ) = 1 )