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 2NN

Proof

Step Hyp Ref Expression
1 dvdszrcl 2N2N
2 1 simprd 2NN