Theorem zefldiv2

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

	Ref	Expression
Assertion	zefldiv2	$$⊢\left(N\in \mathbb{Z}\wedge \frac{N}{2}\in \mathbb{Z}\right)\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$

Proof

Step	Hyp	Ref	Expression
1		flid	$$⊢\frac{N}{2}\in \mathbb{Z}\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$
2	1	adantl	$$⊢\left(N\in \mathbb{Z}\wedge \frac{N}{2}\in \mathbb{Z}\right)\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$