Theorem nneven

Description: An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
2		2re	$$⊢2\in ℝ$$
3	2	a1i	$$⊢N\in \mathbb{N}\to 2\in ℝ$$
4		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
5		2pos	$$⊢0<2$$
6	5	a1i	$$⊢N\in \mathbb{N}\to 0<2$$
7	1 3 4 6	divgt0d	$$⊢N\in \mathbb{N}\to 0<\frac{N}{2}$$
8		evendiv2z	$$⊢N\in \mathrm{Even}\to \frac{N}{2}\in \mathbb{Z}$$
9	7 8	anim12ci	$$⊢\left(N\in \mathbb{N}\wedge N\in \mathrm{Even}\right)\to \left(\frac{N}{2}\in \mathbb{Z}\wedge 0<\frac{N}{2}\right)$$
10		elnnz	$$⊢\frac{N}{2}\in \mathbb{N}\leftrightarrow \left(\frac{N}{2}\in \mathbb{Z}\wedge 0<\frac{N}{2}\right)$$
11	9 10	sylibr	$$⊢\left(N\in \mathbb{N}\wedge N\in \mathrm{Even}\right)\to \frac{N}{2}\in \mathbb{N}$$