Theorem evendiv2z

Description: The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020)

	Ref	Expression
Assertion	evendiv2z	$$⊢Z\in \mathrm{Even}\to \frac{Z}{2}\in \mathbb{Z}$$

Proof

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