Metamath Proof Explorer


Theorem evenelz

Description: An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl . (Contributed by AV, 22-Jun-2021)

Ref Expression
Assertion evenelz ( 2 ∥ 𝑁𝑁 ∈ ℤ )

Proof

Step Hyp Ref Expression
1 dvdszrcl ( 2 ∥ 𝑁 → ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 1 simprd ( 2 ∥ 𝑁𝑁 ∈ ℤ )