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		1red	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
12		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℝ$$
13		rehalfcl	$$⊢N\in ℝ\to \frac{N}{2}\in ℝ$$
14	1 2 13	3syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\in ℝ$$
15		2rp	$$⊢2\in {ℝ}^{+}$$
16	15	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\in {ℝ}^{+}$$
17		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le N$$
18		divge1	$$⊢\left(2\in {ℝ}^{+}\wedge N\in ℝ\wedge 2\le N\right)\to 1\le \frac{N}{2}$$
19	16 12 17 18	syl3anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\le \frac{N}{2}$$
20		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℂ$$
21		subhalfhalf	$$⊢N\in ℂ\to N-\left(\frac{N}{2}\right)=\frac{N}{2}$$
22	20 21	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-\left(\frac{N}{2}\right)=\frac{N}{2}$$
23	19 22	breqtrrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\le N-\left(\frac{N}{2}\right)$$
24	11 12 14 23	lesubd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\le N-1$$
25		2t2e4	$$⊢2\cdot 2=4$$
26	25	eqcomi	$$⊢4=2\cdot 2$$
27	26	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 4=2\cdot 2$$
28	27	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}=\frac{N}{2\cdot 2}$$
29		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
30	29	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2\in ℂ\wedge 2\ne 0\right)$$
31		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}$$
32	20 30 30 31	syl3anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{\frac{N}{2}}{2}=\frac{N}{2\cdot 2}$$
33	28 32	eqtr4d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}=\frac{\frac{N}{2}}{2}$$
34	33	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)$$
35		peano2rem	$$⊢N\in ℝ\to N-1\in ℝ$$
36	12 35	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in ℝ$$
37	14 36 16	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)$$
38	34 37	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)$$
39	24 38	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{4}\le \frac{N-1}{2}$$
40	8	flcld	$$⊢N\in ℝ\to ⌊\frac{N}{4}⌋\in \mathbb{Z}$$
41	40	zred	$$⊢N\in ℝ\to ⌊\frac{N}{4}⌋\in ℝ$$
42	35	rehalfcld	$$⊢N\in ℝ\to \frac{N-1}{2}\in ℝ$$
43	41 8 42	3jca	$$⊢N\in ℝ\to \left(⌊\frac{N}{4}⌋\in ℝ\wedge \frac{N}{4}\in ℝ\wedge \frac{N-1}{2}\in ℝ\right)$$
44		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)$$
45	1 2 43 44	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)$$
46	10 39 45	mp2and	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌊\frac{N}{4}⌋\le \frac{N-1}{2}$$