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 eqeltrdi ⊢ 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 biimtrrdi ⊢ 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 2div2e1 ⊢ 2 2 = 1
54 53 eqcomi ⊢ 1 = 2 2
55 54 oveq2i ⊢ - N + 1 2 − 1 = - N + 1 2 − 2 2
56 peano2cn ⊢ − N ∈ ℂ → - N + 1 ∈ ℂ
57 45 56 syl ⊢ N ∈ ℂ → - N + 1 ∈ ℂ
58 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
59 divsubdir ⊢ - N + 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → -N + 1 - 2 2 = - N + 1 2 − 2 2
60 3 58 59 mp3an23 ⊢ - N + 1 ∈ ℂ → -N + 1 - 2 2 = - N + 1 2 − 2 2
61 57 60 syl ⊢ N ∈ ℂ → -N + 1 - 2 2 = - N + 1 2 − 2 2
62 55 61 eqtr4id ⊢ 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 imbitrid ⊢ 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 ∈ ℤ