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 biimtrrdi 
 |-  ( 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 imbitrid 
 |-  ( 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 ) )