# Metamath Proof Explorer

## Theorem zeo

Description: An integer is even or odd. (Contributed by NM, 1-Jan-2006)

Ref Expression
Assertion zeo ${⊢}{N}\in ℤ\to \left(\frac{{N}}{2}\in ℤ\vee \frac{{N}+1}{2}\in ℤ\right)$

### Proof

Step Hyp Ref Expression
1 elz ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)$
2 oveq1 ${⊢}{N}=0\to \frac{{N}}{2}=\frac{0}{2}$
3 2cn ${⊢}2\in ℂ$
4 2ne0 ${⊢}2\ne 0$
5 3 4 div0i ${⊢}\frac{0}{2}=0$
6 0z ${⊢}0\in ℤ$
7 5 6 eqeltri ${⊢}\frac{0}{2}\in ℤ$
8 2 7 syl6eqel ${⊢}{N}=0\to \frac{{N}}{2}\in ℤ$
9 8 pm2.24d ${⊢}{N}=0\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
10 9 adantl ${⊢}\left({N}\in ℝ\wedge {N}=0\right)\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
11 nnz ${⊢}\frac{{N}}{2}\in ℕ\to \frac{{N}}{2}\in ℤ$
12 11 con3i ${⊢}¬\frac{{N}}{2}\in ℤ\to ¬\frac{{N}}{2}\in ℕ$
13 nneo ${⊢}{N}\in ℕ\to \left(\frac{{N}}{2}\in ℕ↔¬\frac{{N}+1}{2}\in ℕ\right)$
14 13 biimprd ${⊢}{N}\in ℕ\to \left(¬\frac{{N}+1}{2}\in ℕ\to \frac{{N}}{2}\in ℕ\right)$
15 14 con1d ${⊢}{N}\in ℕ\to \left(¬\frac{{N}}{2}\in ℕ\to \frac{{N}+1}{2}\in ℕ\right)$
16 nnz ${⊢}\frac{{N}+1}{2}\in ℕ\to \frac{{N}+1}{2}\in ℤ$
17 12 15 16 syl56 ${⊢}{N}\in ℕ\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
18 17 adantl ${⊢}\left({N}\in ℝ\wedge {N}\in ℕ\right)\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
19 recn ${⊢}{N}\in ℝ\to {N}\in ℂ$
20 divneg ${⊢}\left({N}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{{N}}{2}=\frac{-{N}}{2}$
21 3 4 20 mp3an23 ${⊢}{N}\in ℂ\to -\frac{{N}}{2}=\frac{-{N}}{2}$
22 19 21 syl ${⊢}{N}\in ℝ\to -\frac{{N}}{2}=\frac{-{N}}{2}$
23 22 eleq1d ${⊢}{N}\in ℝ\to \left(-\frac{{N}}{2}\in ℕ↔\frac{-{N}}{2}\in ℕ\right)$
24 nnnegz ${⊢}-\frac{{N}}{2}\in ℕ\to -\left(-\frac{{N}}{2}\right)\in ℤ$
25 23 24 syl6bir ${⊢}{N}\in ℝ\to \left(\frac{-{N}}{2}\in ℕ\to -\left(-\frac{{N}}{2}\right)\in ℤ\right)$
26 19 halfcld ${⊢}{N}\in ℝ\to \frac{{N}}{2}\in ℂ$
27 26 negnegd ${⊢}{N}\in ℝ\to -\left(-\frac{{N}}{2}\right)=\frac{{N}}{2}$
28 27 eleq1d ${⊢}{N}\in ℝ\to \left(-\left(-\frac{{N}}{2}\right)\in ℤ↔\frac{{N}}{2}\in ℤ\right)$
29 25 28 sylibd ${⊢}{N}\in ℝ\to \left(\frac{-{N}}{2}\in ℕ\to \frac{{N}}{2}\in ℤ\right)$
30 29 adantr ${⊢}\left({N}\in ℝ\wedge -{N}\in ℕ\right)\to \left(\frac{-{N}}{2}\in ℕ\to \frac{{N}}{2}\in ℤ\right)$
31 30 con3d ${⊢}\left({N}\in ℝ\wedge -{N}\in ℕ\right)\to \left(¬\frac{{N}}{2}\in ℤ\to ¬\frac{-{N}}{2}\in ℕ\right)$
32 nneo ${⊢}-{N}\in ℕ\to \left(\frac{-{N}}{2}\in ℕ↔¬\frac{-{N}+1}{2}\in ℕ\right)$
33 32 biimprd ${⊢}-{N}\in ℕ\to \left(¬\frac{-{N}+1}{2}\in ℕ\to \frac{-{N}}{2}\in ℕ\right)$
34 33 con1d ${⊢}-{N}\in ℕ\to \left(¬\frac{-{N}}{2}\in ℕ\to \frac{-{N}+1}{2}\in ℕ\right)$
35 nnz ${⊢}\frac{-{N}+1}{2}\in ℕ\to \frac{-{N}+1}{2}\in ℤ$
36 peano2zm ${⊢}\frac{-{N}+1}{2}\in ℤ\to \left(\frac{-{N}+1}{2}\right)-1\in ℤ$
37 ax-1cn ${⊢}1\in ℂ$
38 37 3 negsubdi2i ${⊢}-\left(1-2\right)=2-1$
39 2m1e1 ${⊢}2-1=1$
40 38 39 eqtr2i ${⊢}1=-\left(1-2\right)$
41 37 3 subcli ${⊢}1-2\in ℂ$
42 37 41 negcon2i ${⊢}1=-\left(1-2\right)↔1-2=-1$
43 40 42 mpbi ${⊢}1-2=-1$
44 43 oveq2i ${⊢}-{N}+1-2=-{N}+-1$
45 negcl ${⊢}{N}\in ℂ\to -{N}\in ℂ$
46 addsubass ${⊢}\left(-{N}\in ℂ\wedge 1\in ℂ\wedge 2\in ℂ\right)\to -{N}+1-2=-{N}+1-2$
47 37 3 46 mp3an23 ${⊢}-{N}\in ℂ\to -{N}+1-2=-{N}+1-2$
48 45 47 syl ${⊢}{N}\in ℂ\to -{N}+1-2=-{N}+1-2$
49 negdi ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\to -\left({N}+1\right)=-{N}+-1$
50 37 49 mpan2 ${⊢}{N}\in ℂ\to -\left({N}+1\right)=-{N}+-1$
51 44 48 50 3eqtr4a ${⊢}{N}\in ℂ\to -{N}+1-2=-\left({N}+1\right)$
52 51 oveq1d ${⊢}{N}\in ℂ\to \frac{-{N}+1-2}{2}=\frac{-\left({N}+1\right)}{2}$
53 peano2cn ${⊢}-{N}\in ℂ\to -{N}+1\in ℂ$
54 45 53 syl ${⊢}{N}\in ℂ\to -{N}+1\in ℂ$
55 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
56 divsubdir ${⊢}\left(-{N}+1\in ℂ\wedge 2\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{-{N}+1-2}{2}=\left(\frac{-{N}+1}{2}\right)-\left(\frac{2}{2}\right)$
57 3 55 56 mp3an23 ${⊢}-{N}+1\in ℂ\to \frac{-{N}+1-2}{2}=\left(\frac{-{N}+1}{2}\right)-\left(\frac{2}{2}\right)$
58 54 57 syl ${⊢}{N}\in ℂ\to \frac{-{N}+1-2}{2}=\left(\frac{-{N}+1}{2}\right)-\left(\frac{2}{2}\right)$
59 2div2e1 ${⊢}\frac{2}{2}=1$
60 59 eqcomi ${⊢}1=\frac{2}{2}$
61 60 oveq2i ${⊢}\left(\frac{-{N}+1}{2}\right)-1=\left(\frac{-{N}+1}{2}\right)-\left(\frac{2}{2}\right)$
62 58 61 syl6reqr ${⊢}{N}\in ℂ\to \left(\frac{-{N}+1}{2}\right)-1=\frac{-{N}+1-2}{2}$
63 peano2cn ${⊢}{N}\in ℂ\to {N}+1\in ℂ$
64 divneg ${⊢}\left({N}+1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{{N}+1}{2}=\frac{-\left({N}+1\right)}{2}$
65 3 4 64 mp3an23 ${⊢}{N}+1\in ℂ\to -\frac{{N}+1}{2}=\frac{-\left({N}+1\right)}{2}$
66 63 65 syl ${⊢}{N}\in ℂ\to -\frac{{N}+1}{2}=\frac{-\left({N}+1\right)}{2}$
67 52 62 66 3eqtr4d ${⊢}{N}\in ℂ\to \left(\frac{-{N}+1}{2}\right)-1=-\frac{{N}+1}{2}$
68 19 67 syl ${⊢}{N}\in ℝ\to \left(\frac{-{N}+1}{2}\right)-1=-\frac{{N}+1}{2}$
69 68 eleq1d ${⊢}{N}\in ℝ\to \left(\left(\frac{-{N}+1}{2}\right)-1\in ℤ↔-\frac{{N}+1}{2}\in ℤ\right)$
70 36 69 syl5ib ${⊢}{N}\in ℝ\to \left(\frac{-{N}+1}{2}\in ℤ\to -\frac{{N}+1}{2}\in ℤ\right)$
71 znegcl ${⊢}-\frac{{N}+1}{2}\in ℤ\to -\left(-\frac{{N}+1}{2}\right)\in ℤ$
72 70 71 syl6 ${⊢}{N}\in ℝ\to \left(\frac{-{N}+1}{2}\in ℤ\to -\left(-\frac{{N}+1}{2}\right)\in ℤ\right)$
73 peano2re ${⊢}{N}\in ℝ\to {N}+1\in ℝ$
74 73 recnd ${⊢}{N}\in ℝ\to {N}+1\in ℂ$
75 74 halfcld ${⊢}{N}\in ℝ\to \frac{{N}+1}{2}\in ℂ$
76 75 negnegd ${⊢}{N}\in ℝ\to -\left(-\frac{{N}+1}{2}\right)=\frac{{N}+1}{2}$
77 76 eleq1d ${⊢}{N}\in ℝ\to \left(-\left(-\frac{{N}+1}{2}\right)\in ℤ↔\frac{{N}+1}{2}\in ℤ\right)$
78 72 77 sylibd ${⊢}{N}\in ℝ\to \left(\frac{-{N}+1}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
79 35 78 syl5 ${⊢}{N}\in ℝ\to \left(\frac{-{N}+1}{2}\in ℕ\to \frac{{N}+1}{2}\in ℤ\right)$
80 34 79 sylan9r ${⊢}\left({N}\in ℝ\wedge -{N}\in ℕ\right)\to \left(¬\frac{-{N}}{2}\in ℕ\to \frac{{N}+1}{2}\in ℤ\right)$
81 31 80 syld ${⊢}\left({N}\in ℝ\wedge -{N}\in ℕ\right)\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
82 10 18 81 3jaodan ${⊢}\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
83 1 82 sylbi ${⊢}{N}\in ℤ\to \left(¬\frac{{N}}{2}\in ℤ\to \frac{{N}+1}{2}\in ℤ\right)$
84 83 orrd ${⊢}{N}\in ℤ\to \left(\frac{{N}}{2}\in ℤ\vee \frac{{N}+1}{2}\in ℤ\right)$