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 \in Even \to {(- 1)}^{N} = 1$

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ n = N \to (n = 2 i \leftrightarrow N = 2 i)$
2	1	rexbidv	$⊢ n = N \to (\exists i \in ℤ n = 2 i \leftrightarrow \exists i \in ℤ N = 2 i)$
3		dfeven4	$⊢ Even = \{n \in ℤ \| \exists i \in ℤ n = 2 i\}$
4	2 3	elrab2	$⊢ N \in Even \leftrightarrow (N \in ℤ \land \exists i \in ℤ N = 2 i)$
5		oveq2	$⊢ N = 2 i \to {(- 1)}^{N} = {(- 1)}^{2 i}$
6		neg1cn	$⊢ - 1 \in ℂ$
7	6	a1i	$⊢ i \in ℤ \to - 1 \in ℂ$
8		neg1ne0	$⊢ - 1 \neq 0$
9	8	a1i	$⊢ i \in ℤ \to - 1 \neq 0$
10		2z	$⊢ 2 \in ℤ$
11	10	a1i	$⊢ i \in ℤ \to 2 \in ℤ$
12		id	$⊢ i \in ℤ \to i \in ℤ$
13		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land i \in ℤ)) \to {(- 1)}^{2 i} = {({-1}^{2})}^{i}$
14	7 9 11 12 13	syl22anc	$⊢ i \in ℤ \to {(- 1)}^{2 i} = {({-1}^{2})}^{i}$
15		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
16	15	oveq1i	$⊢ {({-1}^{2})}^{i} = 1^{i}$
17		1exp	$⊢ i \in ℤ \to 1^{i} = 1$
18	16 17	eqtrid	$⊢ i \in ℤ \to {({-1}^{2})}^{i} = 1$
19	14 18	eqtrd	$⊢ i \in ℤ \to {(- 1)}^{2 i} = 1$
20	19	adantl	$⊢ (N \in ℤ \land i \in ℤ) \to {(- 1)}^{2 i} = 1$
21	5 20	sylan9eqr	$⊢ ((N \in ℤ \land i \in ℤ) \land N = 2 i) \to {(- 1)}^{N} = 1$
22	21	rexlimdva2	$⊢ N \in ℤ \to (\exists i \in ℤ N = 2 i \to {(- 1)}^{N} = 1)$
23	22	imp	$⊢ (N \in ℤ \land \exists i \in ℤ N = 2 i) \to {(- 1)}^{N} = 1$
24	4 23	sylbi	$⊢ N \in Even \to {(- 1)}^{N} = 1$

Metamath Proof Explorer