Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Alternate definitions using the "divides" relation
m2even
Next ⟩
2ndvdsodd
Metamath Proof Explorer
Ascii
Unicode
Theorem
m2even
Description:
A multiple of 2 is an even number.
(Contributed by
AV
, 5-Jun-2023)
Ref
Expression
Assertion
m2even
⊢
Z
∈
ℤ
→
2
⁢
Z
∈
Even
Proof
Step
Hyp
Ref
Expression
1
2z
⊢
2
∈
ℤ
2
1
a1i
⊢
Z
∈
ℤ
→
2
∈
ℤ
3
id
⊢
Z
∈
ℤ
→
Z
∈
ℤ
4
2
3
zmulcld
⊢
Z
∈
ℤ
→
2
⁢
Z
∈
ℤ
5
dvdsmul1
⊢
2
∈
ℤ
∧
Z
∈
ℤ
→
2
∥
2
⁢
Z
6
1
5
mpan
⊢
Z
∈
ℤ
→
2
∥
2
⁢
Z
7
iseven2
⊢
2
⁢
Z
∈
Even
↔
2
⁢
Z
∈
ℤ
∧
2
∥
2
⁢
Z
8
4
6
7
sylanbrc
⊢
Z
∈
ℤ
→
2
⁢
Z
∈
Even