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 ∥ 𝑁 → 𝑁 ∈ ℤ )