Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Alternate definitions using the "modulo" operation
dfeven3
Next ⟩
dfodd4
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfeven3
Description:
Alternate definition for even numbers.
(Contributed by
AV
, 18-Jun-2020)
Ref
Expression
Assertion
dfeven3
⊢
Even
=
z
∈
ℤ
|
z
mod
2
=
0
Proof
Step
Hyp
Ref
Expression
1
df-even
⊢
Even
=
z
∈
ℤ
|
z
2
∈
ℤ
2
zre
⊢
z
∈
ℤ
→
z
∈
ℝ
3
2rp
⊢
2
∈
ℝ
+
4
mod0
⊢
z
∈
ℝ
∧
2
∈
ℝ
+
→
z
mod
2
=
0
↔
z
2
∈
ℤ
5
2
3
4
sylancl
⊢
z
∈
ℤ
→
z
mod
2
=
0
↔
z
2
∈
ℤ
6
5
bicomd
⊢
z
∈
ℤ
→
z
2
∈
ℤ
↔
z
mod
2
=
0
7
6
rabbiia
⊢
z
∈
ℤ
|
z
2
∈
ℤ
=
z
∈
ℤ
|
z
mod
2
=
0
8
1
7
eqtri
⊢
Even
=
z
∈
ℤ
|
z
mod
2
=
0