Theorem 2ltceilhalf

Description: The ceiling of half of an integer greater than 2 is greater than or equal to 2. (Contributed by AV, 4-Sep-2025)

	Ref	Expression
Assertion	2ltceilhalf	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\le ⌈\frac{N}{2}⌉$$

Proof

Step	Hyp	Ref	Expression
1		uzp1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(N=3\vee N\in {\mathbb{Z}}_{\ge \left(3+1\right)}\right)$$
2		ex-ceil	$$⊢\left(⌈\frac{3}{2}⌉=2\wedge ⌈-\frac{3}{2}⌉=-1\right)$$
3		2re	$$⊢2\in ℝ$$
4	3	leidi	$$⊢2\le 2$$
5		breq2	$$⊢⌈\frac{3}{2}⌉=2\to \left(2\le ⌈\frac{3}{2}⌉\leftrightarrow 2\le 2\right)$$
6	4 5	mpbiri	$$⊢⌈\frac{3}{2}⌉=2\to 2\le ⌈\frac{3}{2}⌉$$
7	6	adantr	$$⊢\left(⌈\frac{3}{2}⌉=2\wedge ⌈-\frac{3}{2}⌉=-1\right)\to 2\le ⌈\frac{3}{2}⌉$$
8	2 7	ax-mp	$$⊢2\le ⌈\frac{3}{2}⌉$$
9		fvoveq1	$$⊢N=3\to ⌈\frac{N}{2}⌉=⌈\frac{3}{2}⌉$$
10	8 9	breqtrrid	$$⊢N=3\to 2\le ⌈\frac{N}{2}⌉$$
11	3	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2\in ℝ$$
12		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to N\in ℝ$$
13	12	rehalfcld	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to \frac{N}{2}\in ℝ$$
14	13	ceilcld	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
15	14	zred	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to ⌈\frac{N}{2}⌉\in ℝ$$
16		2t2e4	$$⊢2\cdot 2=4$$
17		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 4\le N$$
18	16 17	eqbrtrid	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2\cdot 2\le N$$
19		2pos	$$⊢0<2$$
20	3 19	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
21	20	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to \left(2\in ℝ\wedge 0<2\right)$$
22		lemuldiv	$$⊢\left(2\in ℝ\wedge N\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(2\cdot 2\le N\leftrightarrow 2\le \frac{N}{2}\right)$$
23	3 12 21 22	mp3an2i	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to \left(2\cdot 2\le N\leftrightarrow 2\le \frac{N}{2}\right)$$
24	18 23	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2\le \frac{N}{2}$$
25	13	ceilged	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to \frac{N}{2}\le ⌈\frac{N}{2}⌉$$
26	11 13 15 24 25	letrd	$$⊢N\in {\mathbb{Z}}_{\ge 4}\to 2\le ⌈\frac{N}{2}⌉$$
27		3p1e4	$$⊢3+1=4$$
28	27	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(3+1\right)}={\mathbb{Z}}_{\ge 4}$$
29	26 28	eleq2s	$$⊢N\in {\mathbb{Z}}_{\ge \left(3+1\right)}\to 2\le ⌈\frac{N}{2}⌉$$
30	10 29	jaoi	$$⊢\left(N=3\vee N\in {\mathbb{Z}}_{\ge \left(3+1\right)}\right)\to 2\le ⌈\frac{N}{2}⌉$$
31	1 30	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\le ⌈\frac{N}{2}⌉$$