# Metamath Proof Explorer

## Theorem zofldiv2

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

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

### Proof

Step Hyp Ref Expression
1 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
2 npcan1 ${⊢}{N}\in ℂ\to {N}-1+1={N}$
3 2 eqcomd ${⊢}{N}\in ℂ\to {N}={N}-1+1$
4 1 3 syl ${⊢}{N}\in ℤ\to {N}={N}-1+1$
5 4 oveq1d ${⊢}{N}\in ℤ\to \frac{{N}}{2}=\frac{{N}-1+1}{2}$
6 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
7 6 zcnd ${⊢}{N}\in ℤ\to {N}-1\in ℂ$
8 1cnd ${⊢}{N}\in ℤ\to 1\in ℂ$
9 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
10 9 a1i ${⊢}{N}\in ℤ\to \left(2\in ℂ\wedge 2\ne 0\right)$
11 divdir ${⊢}\left({N}-1\in ℂ\wedge 1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{{N}-1+1}{2}=\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)$
12 7 8 10 11 syl3anc ${⊢}{N}\in ℤ\to \frac{{N}-1+1}{2}=\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)$
13 5 12 eqtrd ${⊢}{N}\in ℤ\to \frac{{N}}{2}=\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)$
14 13 fveq2d ${⊢}{N}\in ℤ\to ⌊\frac{{N}}{2}⌋=⌊\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)⌋$
15 14 adantr ${⊢}\left({N}\in ℤ\wedge \frac{{N}+1}{2}\in ℤ\right)\to ⌊\frac{{N}}{2}⌋=⌊\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)⌋$
16 halfge0 ${⊢}0\le \frac{1}{2}$
17 halflt1 ${⊢}\frac{1}{2}<1$
18 16 17 pm3.2i ${⊢}\left(0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)$
19 zob ${⊢}{N}\in ℤ\to \left(\frac{{N}+1}{2}\in ℤ↔\frac{{N}-1}{2}\in ℤ\right)$
20 19 biimpa ${⊢}\left({N}\in ℤ\wedge \frac{{N}+1}{2}\in ℤ\right)\to \frac{{N}-1}{2}\in ℤ$
21 halfre ${⊢}\frac{1}{2}\in ℝ$
22 flbi2 ${⊢}\left(\frac{{N}-1}{2}\in ℤ\wedge \frac{1}{2}\in ℝ\right)\to \left(⌊\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)⌋=\frac{{N}-1}{2}↔\left(0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)\right)$
23 20 21 22 sylancl ${⊢}\left({N}\in ℤ\wedge \frac{{N}+1}{2}\in ℤ\right)\to \left(⌊\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)⌋=\frac{{N}-1}{2}↔\left(0\le \frac{1}{2}\wedge \frac{1}{2}<1\right)\right)$
24 18 23 mpbiri ${⊢}\left({N}\in ℤ\wedge \frac{{N}+1}{2}\in ℤ\right)\to ⌊\left(\frac{{N}-1}{2}\right)+\left(\frac{1}{2}\right)⌋=\frac{{N}-1}{2}$
25 15 24 eqtrd ${⊢}\left({N}\in ℤ\wedge \frac{{N}+1}{2}\in ℤ\right)\to ⌊\frac{{N}}{2}⌋=\frac{{N}-1}{2}$