Theorem fldiv4lem1div2uz2

Description: The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021) (Proof shortened by AV, 9-Jul-2022)

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

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{Z}$$
2		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
3		id	$$⊢N\in ℝ\to N\in ℝ$$
4		4re	$$⊢4\in ℝ$$
5	4	a1i	$$⊢N\in ℝ\to 4\in ℝ$$
6		4ne0	$$⊢4\ne 0$$
7	6	a1i	$$⊢N\in ℝ\to 4\ne 0$$
8	3 5 7	redivcld	$$⊢N\in ℝ\to \frac{N}{4}\in ℝ$$
9		flle	$$⊢\frac{N}{4}\in ℝ\to ⌊\frac{N}{4}⌋\le \frac{N}{4}$$
10	1 2 8 9	4syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌊\frac{N}{4}⌋\le \frac{N}{4}$$
11		ge2halflem1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\le N-1$$
12		2t2e4	$$⊢2\cdot 2=4$$
13	12	eqcomi	$$⊢4=2\cdot 2$$
14	13	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 4=2\cdot 2$$
15	14	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}=\frac{N}{2\cdot 2}$$
16		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℂ$$
17		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
18	17	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2\in ℂ\wedge 2\ne 0\right)$$
19		divdiv1	$$⊢\left(N\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\frac{N}{2}}{2}=\frac{N}{2\cdot 2}$$
20	16 18 18 19	syl3anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{\frac{N}{2}}{2}=\frac{N}{2\cdot 2}$$
21	15 20	eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}=\frac{\frac{N}{2}}{2}$$
22	21	breq1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{N}{4}\le \frac{N-1}{2}\leftrightarrow \frac{\frac{N}{2}}{2}\le \frac{N-1}{2}\right)$$
23		rehalfcl	$$⊢N\in ℝ\to \frac{N}{2}\in ℝ$$
24	1 2 23	3syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\in ℝ$$
25		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℝ$$
26		peano2rem	$$⊢N\in ℝ\to N-1\in ℝ$$
27	25 26	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in ℝ$$
28		2rp	$$⊢2\in {ℝ}^{+}$$
29	28	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in {ℝ}^{+}$$
30	24 27 29	lediv1d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{N}{2}\le N-1\leftrightarrow \frac{\frac{N}{2}}{2}\le \frac{N-1}{2}\right)$$
31	22 30	bitr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{N}{4}\le \frac{N-1}{2}\leftrightarrow \frac{N}{2}\le N-1\right)$$
32	11 31	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}\le \frac{N-1}{2}$$
33	8	flcld	$$⊢N\in ℝ\to ⌊\frac{N}{4}⌋\in \mathbb{Z}$$
34	33	zred	$$⊢N\in ℝ\to ⌊\frac{N}{4}⌋\in ℝ$$
35	26	rehalfcld	$$⊢N\in ℝ\to \frac{N-1}{2}\in ℝ$$
36	34 8 35	3jca	$$⊢N\in ℝ\to \left(⌊\frac{N}{4}⌋\in ℝ\wedge \frac{N}{4}\in ℝ\wedge \frac{N-1}{2}\in ℝ\right)$$
37		letr	$$⊢\left(⌊\frac{N}{4}⌋\in ℝ\wedge \frac{N}{4}\in ℝ\wedge \frac{N-1}{2}\in ℝ\right)\to \left(\left(⌊\frac{N}{4}⌋\le \frac{N}{4}\wedge \frac{N}{4}\le \frac{N-1}{2}\right)\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}\right)$$
38	1 2 36 37	4syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\left(⌊\frac{N}{4}⌋\le \frac{N}{4}\wedge \frac{N}{4}\le \frac{N-1}{2}\right)\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}\right)$$
39	10 32 38	mp2and	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$