Theorem zefldiv2ALTV

Description: The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020) (Revised by AV, 18-Jun-2020)

	Ref	Expression
Assertion	zefldiv2ALTV	$$⊢N\in \mathrm{Even}\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$

Proof

Step	Hyp	Ref	Expression
1		evendiv2z	$$⊢N\in \mathrm{Even}\to \frac{N}{2}\in \mathbb{Z}$$
2		flid	$$⊢\frac{N}{2}\in \mathbb{Z}\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$
3	1 2	syl	$$⊢N\in \mathrm{Even}\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$