Theorem nneven

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

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

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2		2re	⊢ 2 ∈ ℝ
3	2	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
4		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
5		2pos	⊢ 0 < 2
6	5	a1i	⊢ ( 𝑁 ∈ ℕ → 0 < 2 )
7	1 3 4 6	divgt0d	⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 / 2 ) )
8		evendiv2z	⊢ ( 𝑁 ∈ Even → ( 𝑁 / 2 ) ∈ ℤ )
9	7 8	anim12ci	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 < ( 𝑁 / 2 ) ) )
10		elnnz	⊢ ( ( 𝑁 / 2 ) ∈ ℕ ↔ ( ( 𝑁 / 2 ) ∈ ℤ ∧ 0 < ( 𝑁 / 2 ) ) )
11	9 10	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → ( 𝑁 / 2 ) ∈ ℕ )