Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
zeo
Next ⟩
zeo2
Metamath Proof Explorer
Ascii
Unicode
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
syl6bir
⊢
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
syl5ib
⊢
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
∈
ℤ