Description: Exponentiation of -1 by an even power. Variant of m1expeven . (Contributed by AV, 25-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | m1expe | ⊢ ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | even2n | ⊢ ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 ) | |
2 | oveq2 | ⊢ ( 𝑁 = ( 2 · 𝑛 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) ) | |
3 | 2 | eqcoms | ⊢ ( ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) ) |
4 | m1expeven | ⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 ) | |
5 | 3 4 | sylan9eqr | ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 2 · 𝑛 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 ) |
6 | 5 | rexlimiva | ⊢ ( ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) |
7 | 1 6 | sylbi | ⊢ ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) |