Theorem nn0e

Description: An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
2		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
3		2re	$$⊢2\in ℝ$$
4	3	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℝ$$
5		2pos	$$⊢0<2$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to 0<2$$
7		ge0div	$$⊢\left(N\in ℝ\wedge 2\in ℝ\wedge 0<2\right)\to \left(0\le N\leftrightarrow 0\le \frac{N}{2}\right)$$
8	2 4 6 7	syl3anc	$$⊢N\in {\mathbb{N}}_0\to \left(0\le N\leftrightarrow 0\le \frac{N}{2}\right)$$
9	1 8	mpbid	$$⊢N\in {\mathbb{N}}_0\to 0\le \frac{N}{2}$$
10		evendiv2z	$$⊢N\in \mathrm{Even}\to \frac{N}{2}\in \mathbb{Z}$$
11	9 10	anim12ci	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\in \mathrm{Even}\right)\to \left(\frac{N}{2}\in \mathbb{Z}\wedge 0\le \frac{N}{2}\right)$$
12		elnn0z	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\leftrightarrow \left(\frac{N}{2}\in \mathbb{Z}\wedge 0\le \frac{N}{2}\right)$$
13	11 12	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\in \mathrm{Even}\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$