Theorem flnn0div2ge

Description: The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		nn0eo	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N}{2}\in {\mathbb{N}}_0\vee \frac{N+1}{2}\in {\mathbb{N}}_0\right)$$
2		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
3		peano2rem	$$⊢N\in ℝ\to N-1\in ℝ$$
4	2 3	syl	$$⊢N\in {\mathbb{N}}_0\to N-1\in ℝ$$
5	4	adantl	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N-1\in ℝ$$
6	2	adantl	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N\in ℝ$$
7		2rp	$$⊢2\in {ℝ}^{+}$$
8	7	a1i	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to 2\in {ℝ}^{+}$$
9	2	lem1d	$$⊢N\in {\mathbb{N}}_0\to N-1\le N$$
10	9	adantl	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N-1\le N$$
11	5 6 8 10	lediv1dd	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\le \frac{N}{2}$$
12		nn0z	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\to \frac{N}{2}\in \mathbb{Z}$$
13		flid	$$⊢\frac{N}{2}\in \mathbb{Z}\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$
14	12 13	syl	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$
15	14	adantr	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to ⌊\frac{N}{2}⌋=\frac{N}{2}$$
16	11 15	breqtrrd	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋$$
17	16	ex	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\to \left(N\in {\mathbb{N}}_0\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋\right)$$
18		nn0o	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
19	18	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
20		nn0z	$$⊢\frac{N-1}{2}\in {\mathbb{N}}_0\to \frac{N-1}{2}\in \mathbb{Z}$$
21	20	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in \mathbb{Z}$$
22		flid	$$⊢\frac{N-1}{2}\in \mathbb{Z}\to ⌊\frac{N-1}{2}⌋=\frac{N-1}{2}$$
23	21 22	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to ⌊\frac{N-1}{2}⌋=\frac{N-1}{2}$$
24	4	rehalfcld	$$⊢N\in {\mathbb{N}}_0\to \frac{N-1}{2}\in ℝ$$
25	24	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in ℝ$$
26	2	rehalfcld	$$⊢N\in {\mathbb{N}}_0\to \frac{N}{2}\in ℝ$$
27	26	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N}{2}\in ℝ$$
28		2re	$$⊢2\in ℝ$$
29		2pos	$$⊢0<2$$
30	28 29	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
31	30	a1i	$$⊢N\in {\mathbb{N}}_0\to \left(2\in ℝ\wedge 0<2\right)$$
32		lediv1	$$⊢\left(N-1\in ℝ\wedge N\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(N-1\le N\leftrightarrow \frac{N-1}{2}\le \frac{N}{2}\right)$$
33	4 2 31 32	syl3anc	$$⊢N\in {\mathbb{N}}_0\to \left(N-1\le N\leftrightarrow \frac{N-1}{2}\le \frac{N}{2}\right)$$
34	9 33	mpbid	$$⊢N\in {\mathbb{N}}_0\to \frac{N-1}{2}\le \frac{N}{2}$$
35	34	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\le \frac{N}{2}$$
36		flwordi	$$⊢\left(\frac{N-1}{2}\in ℝ\wedge \frac{N}{2}\in ℝ\wedge \frac{N-1}{2}\le \frac{N}{2}\right)\to ⌊\frac{N-1}{2}⌋\le ⌊\frac{N}{2}⌋$$
37	25 27 35 36	syl3anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to ⌊\frac{N-1}{2}⌋\le ⌊\frac{N}{2}⌋$$
38	23 37	eqbrtrrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋$$
39	38	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N-1}{2}\in {\mathbb{N}}_0\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋\right)$$
40	19 39	syldc	$$⊢\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N\in {\mathbb{N}}_0\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋\right)$$
41	17 40	jaoi	$$⊢\left(\frac{N}{2}\in {\mathbb{N}}_0\vee \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \left(N\in {\mathbb{N}}_0\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋\right)$$
42	1 41	mpcom	$$⊢N\in {\mathbb{N}}_0\to \frac{N-1}{2}\le ⌊\frac{N}{2}⌋$$