Metamath Proof Explorer


Theorem zeo

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

Ref Expression
Assertion zeo
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )

Proof

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