Theorem nn0ofldiv2

Description: The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020) (Proof shortened by AV, 7-Jun-2020)

	Ref	Expression
Assertion	nn0ofldiv2	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to ⌊\frac{N}{2}⌋=\frac{N-1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		nn0z	$$⊢\frac{N+1}{2}\in {\mathbb{N}}_0\to \frac{N+1}{2}\in \mathbb{Z}$$
3		zofldiv2	$$⊢\left(N\in \mathbb{Z}\wedge \frac{N+1}{2}\in \mathbb{Z}\right)\to ⌊\frac{N}{2}⌋=\frac{N-1}{2}$$
4	1 2 3	syl2an	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to ⌊\frac{N}{2}⌋=\frac{N-1}{2}$$