Theorem nnpw2even

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

	Ref	Expression
Assertion	nnpw2even	$$⊢N\in \mathbb{N}\to \frac{2^N}{2}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
2		2ne0	$$⊢2\ne 0$$
3	2	a1i	$$⊢N\in \mathbb{N}\to 2\ne 0$$
4		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
5	1 3 4	expm1d	$$⊢N\in \mathbb{N}\to 2^{N-1}=\frac{2^N}{2}$$
6		2nn	$$⊢2\in \mathbb{N}$$
7	6	a1i	$$⊢N\in \mathbb{N}\to 2\in \mathbb{N}$$
8		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
9	7 8	nnexpcld	$$⊢N\in \mathbb{N}\to 2^{N-1}\in \mathbb{N}$$
10	5 9	eqeltrrd	$$⊢N\in \mathbb{N}\to \frac{2^N}{2}\in \mathbb{N}$$