Theorem 2dvdseven

Description: 2 divides an even number. (Contributed by AV, 18-Jun-2020)

	Ref	Expression
Assertion	2dvdseven	$$⊢Z\in \mathrm{Even}\to 2\parallel Z$$

Proof

Step	Hyp	Ref	Expression
1		iseven2	$$⊢Z\in \mathrm{Even}\leftrightarrow \left(Z\in \mathbb{Z}\wedge 2\parallel Z\right)$$
2	1	simprbi	$$⊢Z\in \mathrm{Even}\to 2\parallel Z$$