Theorem nn0e

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

	Ref	Expression
Assertion	nn0e	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → ( 𝑁 / 2 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
2		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
3		2re	⊢ 2 ∈ ℝ
4	3	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
5		2pos	⊢ 0 < 2
6	5	a1i	⊢ ( 𝑁 ∈ ℕ0 → 0 < 2 )
7		ge0div	⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 ) → ( 0 ≤ 𝑁 ↔ 0 ≤ ( 𝑁 / 2 ) ) )
8	2 4 6 7	syl3anc	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ≤ 𝑁 ↔ 0 ≤ ( 𝑁 / 2 ) ) )
9	1 8	mpbid	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( 𝑁 / 2 ) )
10		evendiv2z	⊢ ( 𝑁 ∈ Even → ( 𝑁 / 2 ) ∈ ℤ )
11	9 10	anim12ci	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 / 2 ) ) )
12		elnn0z	⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 / 2 ) ) )
13	11 12	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → ( 𝑁 / 2 ) ∈ ℕ0 )