Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Alternate definitions using the "modulo" operation
dfodd4
Next ⟩
dfodd5
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfodd4
Description:
Alternate definition for odd numbers.
(Contributed by
AV
, 18-Jun-2020)
Ref
Expression
Assertion
dfodd4
⊢
Odd
=
z
∈
ℤ
|
z
mod
2
=
1
Proof
Step
Hyp
Ref
Expression
1
dfodd2
⊢
Odd
=
z
∈
ℤ
|
z
−
1
2
∈
ℤ
2
peano2zm
⊢
z
∈
ℤ
→
z
−
1
∈
ℤ
3
2
zred
⊢
z
∈
ℤ
→
z
−
1
∈
ℝ
4
2rp
⊢
2
∈
ℝ
+
5
mod0
⊢
z
−
1
∈
ℝ
∧
2
∈
ℝ
+
→
z
−
1
mod
2
=
0
↔
z
−
1
2
∈
ℤ
6
3
4
5
sylancl
⊢
z
∈
ℤ
→
z
−
1
mod
2
=
0
↔
z
−
1
2
∈
ℤ
7
zre
⊢
z
∈
ℤ
→
z
∈
ℝ
8
2re
⊢
2
∈
ℝ
9
8
a1i
⊢
z
∈
ℤ
→
2
∈
ℝ
10
1lt2
⊢
1
<
2
11
10
a1i
⊢
z
∈
ℤ
→
1
<
2
12
m1mod0mod1
⊢
z
∈
ℝ
∧
2
∈
ℝ
∧
1
<
2
→
z
−
1
mod
2
=
0
↔
z
mod
2
=
1
13
7
9
11
12
syl3anc
⊢
z
∈
ℤ
→
z
−
1
mod
2
=
0
↔
z
mod
2
=
1
14
6
13
bitr3d
⊢
z
∈
ℤ
→
z
−
1
2
∈
ℤ
↔
z
mod
2
=
1
15
14
rabbiia
⊢
z
∈
ℤ
|
z
−
1
2
∈
ℤ
=
z
∈
ℤ
|
z
mod
2
=
1
16
1
15
eqtri
⊢
Odd
=
z
∈
ℤ
|
z
mod
2
=
1