Metamath Proof Explorer


Theorem zeo

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

Ref Expression
Assertion zeo N N 2 N + 1 2

Proof

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