nn0e

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

		Ref	Expression
	Assertion	nn0e	$⊢ (N \in ℕ_{0} \land N \in Even) \to \frac{N}{2} \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
2		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
3		2re	$⊢ 2 \in ℝ$
4	3	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℝ$
5		2pos	$⊢ 0 < 2$
6	5	a1i	$⊢ N \in ℕ_{0} \to 0 < 2$
7		ge0div	$⊢ (N \in ℝ \land 2 \in ℝ \land 0 < 2) \to (0 \leq N \leftrightarrow 0 \leq \frac{N}{2})$
8	2 4 6 7	syl3anc	$⊢ N \in ℕ_{0} \to (0 \leq N \leftrightarrow 0 \leq \frac{N}{2})$
9	1 8	mpbid	$⊢ N \in ℕ_{0} \to 0 \leq \frac{N}{2}$
10		evendiv2z	$⊢ N \in Even \to \frac{N}{2} \in ℤ$
11	9 10	anim12ci	$⊢ (N \in ℕ_{0} \land N \in Even) \to (\frac{N}{2} \in ℤ \land 0 \leq \frac{N}{2})$
12		elnn0z	$⊢ \frac{N}{2} \in ℕ_{0} \leftrightarrow (\frac{N}{2} \in ℤ \land 0 \leq \frac{N}{2})$
13	11 12	sylibr	$⊢ (N \in ℕ_{0} \land N \in Even) \to \frac{N}{2} \in ℕ_{0}$

Metamath Proof Explorer