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 ( 𝑁 ∈ Even → ( - 1 ↑ 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 = ( 2 · 𝑖 ) ↔ 𝑁 = ( 2 · 𝑖 ) ) )
2 1 rexbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑖 ∈ ℤ 𝑛 = ( 2 · 𝑖 ) ↔ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) )
3 dfeven4 ⊢ Even = { 𝑛 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑛 = ( 2 · 𝑖 ) }
4 2 3 elrab2 ⊢ ( 𝑁 ∈ Even ↔ ( 𝑁 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) )
5 oveq2 ⊢ ( 𝑁 = ( 2 · 𝑖 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑖 ) ) )
6 neg1cn ⊢ - 1 ∈ ℂ
7 6 a1i ⊢ ( 𝑖 ∈ ℤ → - 1 ∈ ℂ )
8 neg1ne0 ⊢ - 1 ≠ 0
9 8 a1i ⊢ ( 𝑖 ∈ ℤ → - 1 ≠ 0 )
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ ( 𝑖 ∈ ℤ → 2 ∈ ℤ )
12 id ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℤ )
13 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ) → ( - 1 ↑ ( 2 · 𝑖 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑖 ) )
14 7 9 11 12 13 syl22anc ⊢ ( 𝑖 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑖 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑖 ) )
15 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
16 15 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ 𝑖 ) = ( 1 ↑ 𝑖 )
17 1exp ⊢ ( 𝑖 ∈ ℤ → ( 1 ↑ 𝑖 ) = 1 )
18 16 17 eqtrid ⊢ ( 𝑖 ∈ ℤ → ( ( - 1 ↑ 2 ) ↑ 𝑖 ) = 1 )
19 14 18 eqtrd ⊢ ( 𝑖 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑖 ) ) = 1 )
20 19 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( - 1 ↑ ( 2 · 𝑖 ) ) = 1 )
21 5 20 sylan9eqr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑁 = ( 2 · 𝑖 ) ) → ( - 1 ↑ 𝑁 ) = 1 )
22 21 rexlimdva2 ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) → ( - 1 ↑ 𝑁 ) = 1 ) )
23 22 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) → ( - 1 ↑ 𝑁 ) = 1 )
24 4 23 sylbi ⊢ ( 𝑁 ∈ Even → ( - 1 ↑ 𝑁 ) = 1 )