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\parallel N\to N\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	$$⊢2\parallel N\to \left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
2	1	simprd	$$⊢2\parallel N\to N\in \mathbb{Z}$$