Metamath Proof Explorer

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	$⊢ N \in ℕ \to 2^{N} \in Even$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3		zexpcl	$⊢ (2 \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℤ$
4	1 2 3	sylancr	$⊢ N \in ℕ \to 2^{N} \in ℤ$
5		iddvdsexp	$⊢ (2 \in ℤ \land N \in ℕ) \to 2 ∥ 2^{N}$
6	1 5	mpan	$⊢ N \in ℕ \to 2 ∥ 2^{N}$
7		iseven2	$⊢ 2^{N} \in Even \leftrightarrow (2^{N} \in ℤ \land 2 ∥ 2^{N})$
8	4 6 7	sylanbrc	$⊢ N \in ℕ \to 2^{N} \in Even$