Metamath Proof Explorer

Theorem nn0eo

Description: A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020)

Ref Expression
Assertion nn0eo ⊢ N ∈ ℕ 0 → N 2 ∈ ℕ 0 ∨ N + 1 2 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
2 zeo ⊢ N ∈ ℤ → N 2 ∈ ℤ ∨ N + 1 2 ∈ ℤ
3 1 2 syl ⊢ N ∈ ℕ 0 → N 2 ∈ ℤ ∨ N + 1 2 ∈ ℤ
4 simpr ⊢ N ∈ ℕ 0 ∧ N 2 ∈ ℤ → N 2 ∈ ℤ
5 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
6 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
7 2re ⊢ 2 ∈ ℝ
8 7 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
9 2pos ⊢ 0 < 2
10 9 a1i ⊢ N ∈ ℕ 0 → 0 < 2
11 divge0 ⊢ N ∈ ℝ ∧ 0 ≤ N ∧ 2 ∈ ℝ ∧ 0 < 2 → 0 ≤ N 2
12 5 6 8 10 11 syl22anc ⊢ N ∈ ℕ 0 → 0 ≤ N 2
13 12 adantr ⊢ N ∈ ℕ 0 ∧ N 2 ∈ ℤ → 0 ≤ N 2
14 elnn0z ⊢ N 2 ∈ ℕ 0 ↔ N 2 ∈ ℤ ∧ 0 ≤ N 2
15 4 13 14 sylanbrc ⊢ N ∈ ℕ 0 ∧ N 2 ∈ ℤ → N 2 ∈ ℕ 0
16 15 ex ⊢ N ∈ ℕ 0 → N 2 ∈ ℤ → N 2 ∈ ℕ 0
17 simpr ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℤ
18 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
19 18 nn0red ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
20 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
21 0le1 ⊢ 0 ≤ 1
22 21 a1i ⊢ N ∈ ℕ 0 → 0 ≤ 1
23 5 20 6 22 addge0d ⊢ N ∈ ℕ 0 → 0 ≤ N + 1
24 divge0 ⊢ N + 1 ∈ ℝ ∧ 0 ≤ N + 1 ∧ 2 ∈ ℝ ∧ 0 < 2 → 0 ≤ N + 1 2
25 19 23 8 10 24 syl22anc ⊢ N ∈ ℕ 0 → 0 ≤ N + 1 2
26 25 adantr ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℤ → 0 ≤ N + 1 2
27 elnn0z ⊢ N + 1 2 ∈ ℕ 0 ↔ N + 1 2 ∈ ℤ ∧ 0 ≤ N + 1 2
28 17 26 27 sylanbrc ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ 0
29 28 ex ⊢ N ∈ ℕ 0 → N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ 0
30 16 29 orim12d ⊢ N ∈ ℕ 0 → N 2 ∈ ℤ ∨ N + 1 2 ∈ ℤ → N 2 ∈ ℕ 0 ∨ N + 1 2 ∈ ℕ 0
31 3 30 mpd ⊢ N ∈ ℕ 0 → N 2 ∈ ℕ 0 ∨ N + 1 2 ∈ ℕ 0