This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )