Theorem nnehalf

Description: The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
2		nn0ehalf	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\parallel N\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$
3	1 2	sylan	$$⊢\left(N\in \mathbb{N}\wedge 2\parallel N\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$
4		nn0enne	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{N}{2}\in \mathbb{N}\right)$$
5	4	adantr	$$⊢\left(N\in \mathbb{N}\wedge 2\parallel N\right)\to \left(\frac{N}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{N}{2}\in \mathbb{N}\right)$$
6	3 5	mpbid	$$⊢\left(N\in \mathbb{N}\wedge 2\parallel N\right)\to \frac{N}{2}\in \mathbb{N}$$