Metamath Proof Explorer


Theorem zeo

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

Ref Expression
Assertion zeo ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 elz ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
2 oveq1 ( 𝑁 = 0 → ( 𝑁 / 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 eqeltrdi ( 𝑁 = 0 → ( 𝑁 / 2 ) ∈ ℤ )
9 8 pm2.24d ( 𝑁 = 0 → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
10 9 adantl ( ( 𝑁 ∈ ℝ ∧ 𝑁 = 0 ) → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
11 nnz ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ )
12 11 con3i ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ¬ ( 𝑁 / 2 ) ∈ ℕ )
13 nneo ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
14 13 biimprd ( 𝑁 ∈ ℕ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
15 14 con1d ( 𝑁 ∈ ℕ → ( ¬ ( 𝑁 / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
16 nnz ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
17 12 15 16 syl56 ( 𝑁 ∈ ℕ → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
18 17 adantl ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
19 recn ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
20 divneg ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 𝑁 / 2 ) = ( - 𝑁 / 2 ) )
21 3 4 20 mp3an23 ( 𝑁 ∈ ℂ → - ( 𝑁 / 2 ) = ( - 𝑁 / 2 ) )
22 19 21 syl ( 𝑁 ∈ ℝ → - ( 𝑁 / 2 ) = ( - 𝑁 / 2 ) )
23 22 eleq1d ( 𝑁 ∈ ℝ → ( - ( 𝑁 / 2 ) ∈ ℕ ↔ ( - 𝑁 / 2 ) ∈ ℕ ) )
24 nnnegz ( - ( 𝑁 / 2 ) ∈ ℕ → - - ( 𝑁 / 2 ) ∈ ℤ )
25 23 24 syl6bir ( 𝑁 ∈ ℝ → ( ( - 𝑁 / 2 ) ∈ ℕ → - - ( 𝑁 / 2 ) ∈ ℤ ) )
26 19 halfcld ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℂ )
27 26 negnegd ( 𝑁 ∈ ℝ → - - ( 𝑁 / 2 ) = ( 𝑁 / 2 ) )
28 27 eleq1d ( 𝑁 ∈ ℝ → ( - - ( 𝑁 / 2 ) ∈ ℤ ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
29 25 28 sylibd ( 𝑁 ∈ ℝ → ( ( - 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ ) )
30 29 adantr ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ( - 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ ) )
31 30 con3d ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ¬ ( - 𝑁 / 2 ) ∈ ℕ ) )
32 nneo ( - 𝑁 ∈ ℕ → ( ( - 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( - 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
33 32 biimprd ( - 𝑁 ∈ ℕ → ( ¬ ( ( - 𝑁 + 1 ) / 2 ) ∈ ℕ → ( - 𝑁 / 2 ) ∈ ℕ ) )
34 33 con1d ( - 𝑁 ∈ ℕ → ( ¬ ( - 𝑁 / 2 ) ∈ ℕ → ( ( - 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
35 nnz ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( - 𝑁 + 1 ) / 2 ) ∈ ℤ )
36 peano2zm ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( ( - 𝑁 + 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 ( - 𝑁 + ( 1 − 2 ) ) = ( - 𝑁 + - 1 )
45 negcl ( 𝑁 ∈ ℂ → - 𝑁 ∈ ℂ )
46 addsubass ( ( - 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( - 𝑁 + 1 ) − 2 ) = ( - 𝑁 + ( 1 − 2 ) ) )
47 37 3 46 mp3an23 ( - 𝑁 ∈ ℂ → ( ( - 𝑁 + 1 ) − 2 ) = ( - 𝑁 + ( 1 − 2 ) ) )
48 45 47 syl ( 𝑁 ∈ ℂ → ( ( - 𝑁 + 1 ) − 2 ) = ( - 𝑁 + ( 1 − 2 ) ) )
49 negdi ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 𝑁 + 1 ) = ( - 𝑁 + - 1 ) )
50 37 49 mpan2 ( 𝑁 ∈ ℂ → - ( 𝑁 + 1 ) = ( - 𝑁 + - 1 ) )
51 44 48 50 3eqtr4a ( 𝑁 ∈ ℂ → ( ( - 𝑁 + 1 ) − 2 ) = - ( 𝑁 + 1 ) )
52 51 oveq1d ( 𝑁 ∈ ℂ → ( ( ( - 𝑁 + 1 ) − 2 ) / 2 ) = ( - ( 𝑁 + 1 ) / 2 ) )
53 2div2e1 ( 2 / 2 ) = 1
54 53 eqcomi 1 = ( 2 / 2 )
55 54 oveq2i ( ( ( - 𝑁 + 1 ) / 2 ) − 1 ) = ( ( ( - 𝑁 + 1 ) / 2 ) − ( 2 / 2 ) )
56 peano2cn ( - 𝑁 ∈ ℂ → ( - 𝑁 + 1 ) ∈ ℂ )
57 45 56 syl ( 𝑁 ∈ ℂ → ( - 𝑁 + 1 ) ∈ ℂ )
58 2cnne0 ( 2 ∈ ℂ ∧ 2 ≠ 0 )
59 divsubdir ( ( ( - 𝑁 + 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( - 𝑁 + 1 ) − 2 ) / 2 ) = ( ( ( - 𝑁 + 1 ) / 2 ) − ( 2 / 2 ) ) )
60 3 58 59 mp3an23 ( ( - 𝑁 + 1 ) ∈ ℂ → ( ( ( - 𝑁 + 1 ) − 2 ) / 2 ) = ( ( ( - 𝑁 + 1 ) / 2 ) − ( 2 / 2 ) ) )
61 57 60 syl ( 𝑁 ∈ ℂ → ( ( ( - 𝑁 + 1 ) − 2 ) / 2 ) = ( ( ( - 𝑁 + 1 ) / 2 ) − ( 2 / 2 ) ) )
62 55 61 eqtr4id ( 𝑁 ∈ ℂ → ( ( ( - 𝑁 + 1 ) / 2 ) − 1 ) = ( ( ( - 𝑁 + 1 ) − 2 ) / 2 ) )
63 peano2cn ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
64 divneg ( ( ( 𝑁 + 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( ( 𝑁 + 1 ) / 2 ) = ( - ( 𝑁 + 1 ) / 2 ) )
65 3 4 64 mp3an23 ( ( 𝑁 + 1 ) ∈ ℂ → - ( ( 𝑁 + 1 ) / 2 ) = ( - ( 𝑁 + 1 ) / 2 ) )
66 63 65 syl ( 𝑁 ∈ ℂ → - ( ( 𝑁 + 1 ) / 2 ) = ( - ( 𝑁 + 1 ) / 2 ) )
67 52 62 66 3eqtr4d ( 𝑁 ∈ ℂ → ( ( ( - 𝑁 + 1 ) / 2 ) − 1 ) = - ( ( 𝑁 + 1 ) / 2 ) )
68 19 67 syl ( 𝑁 ∈ ℝ → ( ( ( - 𝑁 + 1 ) / 2 ) − 1 ) = - ( ( 𝑁 + 1 ) / 2 ) )
69 68 eleq1d ( 𝑁 ∈ ℝ → ( ( ( ( - 𝑁 + 1 ) / 2 ) − 1 ) ∈ ℤ ↔ - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
70 36 69 syl5ib ( 𝑁 ∈ ℝ → ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℤ → - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
71 znegcl ( - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → - - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
72 70 71 syl6 ( 𝑁 ∈ ℝ → ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℤ → - - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
73 peano2re ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
74 73 recnd ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℂ )
75 74 halfcld ( 𝑁 ∈ ℝ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℂ )
76 75 negnegd ( 𝑁 ∈ ℝ → - - ( ( 𝑁 + 1 ) / 2 ) = ( ( 𝑁 + 1 ) / 2 ) )
77 76 eleq1d ( 𝑁 ∈ ℝ → ( - - ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
78 72 77 sylibd ( 𝑁 ∈ ℝ → ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
79 35 78 syl5 ( 𝑁 ∈ ℝ → ( ( ( - 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
80 34 79 sylan9r ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ¬ ( - 𝑁 / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
81 31 80 syld ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
82 10 18 81 3jaodan ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
83 1 82 sylbi ( 𝑁 ∈ ℤ → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
84 83 orrd ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )