Theorem ceilhalfgt1

Description: The ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		1red	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in ℝ$$
2		2re	$$⊢2\in ℝ$$
3	2	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\in ℝ$$
4		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in ℝ$$
5	4	rehalfcld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \frac{N}{2}\in ℝ$$
6	5	ceilcld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
7	6	zred	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in ℝ$$
8		1lt2	$$⊢1<2$$
9	8	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<2$$
10		2ltceilhalf	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\le ⌈\frac{N}{2}⌉$$
11	1 3 7 9 10	ltletrd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<⌈\frac{N}{2}⌉$$