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