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 ∈ Even → − 1 N = 1

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ n = N → n = 2 ⁢ i ↔ N = 2 ⁢ i
2 1 rexbidv ⊢ n = N → ∃ i ∈ ℤ n = 2 ⁢ i ↔ ∃ i ∈ ℤ N = 2 ⁢ i
3 dfeven4 ⊢ Even = n ∈ ℤ | ∃ i ∈ ℤ n = 2 ⁢ i
4 2 3 elrab2 ⊢ N ∈ Even ↔ N ∈ ℤ ∧ ∃ i ∈ ℤ N = 2 ⁢ i
5 oveq2 ⊢ N = 2 ⁢ i → − 1 N = − 1 2 ⁢ i
6 neg1cn ⊢ − 1 ∈ ℂ
7 6 a1i ⊢ i ∈ ℤ → − 1 ∈ ℂ
8 neg1ne0 ⊢ − 1 ≠ 0
9 8 a1i ⊢ i ∈ ℤ → − 1 ≠ 0
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ i ∈ ℤ → 2 ∈ ℤ
12 id ⊢ i ∈ ℤ → i ∈ ℤ
13 expmulz ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ 2 ∈ ℤ ∧ i ∈ ℤ → − 1 2 ⁢ i = -1 2 i
14 7 9 11 12 13 syl22anc ⊢ i ∈ ℤ → − 1 2 ⁢ i = -1 2 i
15 neg1sqe1 ⊢ − 1 2 = 1
16 15 oveq1i ⊢ -1 2 i = 1 i
17 1exp ⊢ i ∈ ℤ → 1 i = 1
18 16 17 eqtrid ⊢ i ∈ ℤ → -1 2 i = 1
19 14 18 eqtrd ⊢ i ∈ ℤ → − 1 2 ⁢ i = 1
20 19 adantl ⊢ N ∈ ℤ ∧ i ∈ ℤ → − 1 2 ⁢ i = 1
21 5 20 sylan9eqr ⊢ N ∈ ℤ ∧ i ∈ ℤ ∧ N = 2 ⁢ i → − 1 N = 1
22 21 rexlimdva2 ⊢ N ∈ ℤ → ∃ i ∈ ℤ N = 2 ⁢ i → − 1 N = 1
23 22 imp ⊢ N ∈ ℤ ∧ ∃ i ∈ ℤ N = 2 ⁢ i → − 1 N = 1
24 4 23 sylbi ⊢ N ∈ Even → − 1 N = 1