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 ) ∈ ℤ ) )