Description: 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nnpw2even | ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 𝑁 ) / 2 ) ∈ ℕ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cnd | ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ ) | |
2 | 2ne0 | ⊢ 2 ≠ 0 | |
3 | 2 | a1i | ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 ) |
4 | nnz | ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ ) | |
5 | 1 3 4 | expm1d | ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) = ( ( 2 ↑ 𝑁 ) / 2 ) ) |
6 | 2nn | ⊢ 2 ∈ ℕ | |
7 | 6 | a1i | ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ ) |
8 | nnm1nn0 | ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 ) | |
9 | 7 8 | nnexpcld | ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℕ ) |
10 | 5 9 | eqeltrrd | ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 𝑁 ) / 2 ) ∈ ℕ ) |