Theorem nnpw2evenALTV

Description: 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020) (Revised by AV, 20-Jun-2020)

	Ref	Expression
Assertion	nnpw2evenALTV	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ Even )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3		zexpcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℤ )
4	1 2 3	sylancr	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℤ )
5		iddvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∥ ( 2 ↑ 𝑁 ) )
6	1 5	mpan	⊢ ( 𝑁 ∈ ℕ → 2 ∥ ( 2 ↑ 𝑁 ) )
7		iseven2	⊢ ( ( 2 ↑ 𝑁 ) ∈ Even ↔ ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ 2 ∥ ( 2 ↑ 𝑁 ) ) )
8	4 6 7	sylanbrc	⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ Even )