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 || N -> N e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	|- ( 2 || N -> ( 2 e. ZZ /\ N e. ZZ ) )
2	1	simprd	|- ( 2 || N -> N e. ZZ )