Theorem fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

	Ref	Expression
Assertion	fldiv4lem1div2	$$⊢N\in \mathbb{N}\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	$$⊢N\in \mathbb{N}\leftrightarrow \left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)$$
2		1lt4	$$⊢1<4$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		4nn	$$⊢4\in \mathbb{N}$$
5		divfl0	$$⊢\left(1\in {\mathbb{N}}_0\wedge 4\in \mathbb{N}\right)\to \left(1<4\leftrightarrow ⌊\frac{1}{4}⌋=0\right)$$
6	3 4 5	mp2an	$$⊢1<4\leftrightarrow ⌊\frac{1}{4}⌋=0$$
7	2 6	mpbi	$$⊢⌊\frac{1}{4}⌋=0$$
8		1re	$$⊢1\in ℝ$$
9		4re	$$⊢4\in ℝ$$
10		4ne0	$$⊢4\ne 0$$
11		redivcl	$$⊢\left(1\in ℝ\wedge 4\in ℝ\wedge 4\ne 0\right)\to \frac{1}{4}\in ℝ$$
12	11	flcld	$$⊢\left(1\in ℝ\wedge 4\in ℝ\wedge 4\ne 0\right)\to ⌊\frac{1}{4}⌋\in \mathbb{Z}$$
13	12	zred	$$⊢\left(1\in ℝ\wedge 4\in ℝ\wedge 4\ne 0\right)\to ⌊\frac{1}{4}⌋\in ℝ$$
14	8 9 10 13	mp3an	$$⊢⌊\frac{1}{4}⌋\in ℝ$$
15	14	eqlei	$$⊢⌊\frac{1}{4}⌋=0\to ⌊\frac{1}{4}⌋\le 0$$
16	7 15	mp1i	$$⊢N=1\to ⌊\frac{1}{4}⌋\le 0$$
17		fvoveq1	$$⊢N=1\to ⌊\frac{N}{4}⌋=⌊\frac{1}{4}⌋$$
18		oveq1	$$⊢N=1\to N-1=1-1$$
19		1m1e0	$$⊢1-1=0$$
20	18 19	eqtrdi	$$⊢N=1\to N-1=0$$
21	20	oveq1d	$$⊢N=1\to \frac{N-1}{2}=\frac{0}{2}$$
22		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
23		div0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)\to \frac{0}{2}=0$$
24	22 23	ax-mp	$$⊢\frac{0}{2}=0$$
25	21 24	eqtrdi	$$⊢N=1\to \frac{N-1}{2}=0$$
26	16 17 25	3brtr4d	$$⊢N=1\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$
27		fldiv4lem1div2uz2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$
28	26 27	jaoi	$$⊢\left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$
29	1 28	sylbi	$$⊢N\in \mathbb{N}\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$