Metamath Proof Explorer

Theorem m1expeven

Description: Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018)

Ref Expression
Assertion m1expeven ⊢ N ∈ ℤ → − 1 2 ⋅ N = 1

Proof

Step Hyp Ref Expression
1 zcn ⊢ N ∈ ℤ → N ∈ ℂ
2 1 2timesd ⊢ N ∈ ℤ → 2 ⋅ N = N + N
3 2 oveq2d ⊢ N ∈ ℤ → − 1 2 ⋅ N = − 1 N + N
4 neg1cn ⊢ − 1 ∈ ℂ
5 neg1ne0 ⊢ − 1 ≠ 0
6 expaddz ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ N ∈ ℤ ∧ N ∈ ℤ → − 1 N + N = − 1 N ⁢ − 1 N
7 4 5 6 mpanl12 ⊢ N ∈ ℤ ∧ N ∈ ℤ → − 1 N + N = − 1 N ⁢ − 1 N
8 7 anidms ⊢ N ∈ ℤ → − 1 N + N = − 1 N ⁢ − 1 N
9 m1expcl2 ⊢ N ∈ ℤ → − 1 N ∈ − 1 1
10 ovex ⊢ − 1 N ∈ V
11 10 elpr ⊢ − 1 N ∈ − 1 1 ↔ − 1 N = − 1 ∨ − 1 N = 1
12 oveq12 ⊢ − 1 N = − 1 ∧ − 1 N = − 1 → − 1 N ⁢ − 1 N = -1 ⁢ -1
13 12 anidms ⊢ − 1 N = − 1 → − 1 N ⁢ − 1 N = -1 ⁢ -1
14 neg1mulneg1e1 ⊢ -1 ⁢ -1 = 1
15 13 14 eqtrdi ⊢ − 1 N = − 1 → − 1 N ⁢ − 1 N = 1
16 oveq12 ⊢ − 1 N = 1 ∧ − 1 N = 1 → − 1 N ⁢ − 1 N = 1 ⋅ 1
17 16 anidms ⊢ − 1 N = 1 → − 1 N ⁢ − 1 N = 1 ⋅ 1
18 1t1e1 ⊢ 1 ⋅ 1 = 1
19 17 18 eqtrdi ⊢ − 1 N = 1 → − 1 N ⁢ − 1 N = 1
20 15 19 jaoi ⊢ − 1 N = − 1 ∨ − 1 N = 1 → − 1 N ⁢ − 1 N = 1
21 11 20 sylbi ⊢ − 1 N ∈ − 1 1 → − 1 N ⁢ − 1 N = 1
22 9 21 syl ⊢ N ∈ ℤ → − 1 N ⁢ − 1 N = 1
23 3 8 22 3eqtrd ⊢ N ∈ ℤ → − 1 2 ⋅ N = 1