Theorem nn0ehalf

Description: The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020) (Revised by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	nn0ehalf	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\parallel N\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		evend2	$$⊢N\in \mathbb{Z}\to \left(2\parallel N\leftrightarrow \frac{N}{2}\in \mathbb{Z}\right)$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\leftrightarrow \frac{N}{2}\in \mathbb{Z}\right)$$
4		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
5		2rp	$$⊢2\in {ℝ}^{+}$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in {ℝ}^{+}$$
7		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
8	4 6 7	divge0d	$$⊢N\in {\mathbb{N}}_0\to 0\le \frac{N}{2}$$
9	8	anim1ci	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in \mathbb{Z}\right)\to \left(\frac{N}{2}\in \mathbb{Z}\wedge 0\le \frac{N}{2}\right)$$
10		elnn0z	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\leftrightarrow \left(\frac{N}{2}\in \mathbb{Z}\wedge 0\le \frac{N}{2}\right)$$
11	9 10	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in \mathbb{Z}\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$
12	11	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N}{2}\in \mathbb{Z}\to \frac{N}{2}\in {\mathbb{N}}_0\right)$$
13	3 12	sylbid	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\to \frac{N}{2}\in {\mathbb{N}}_0\right)$$
14	13	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\parallel N\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$