Theorem 1elfzo1ceilhalf1

Description: 1 is in the half-open integer range from 1 to the ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	1elfzo1ceilhalf1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2	1	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \mathbb{N}$$
3		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
4		ceilhalfnn	$$⊢N\in \mathbb{N}\to ⌈\frac{N}{2}⌉\in \mathbb{N}$$
5	3 4	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to ⌈\frac{N}{2}⌉\in \mathbb{N}$$
6		ceilhalfgt1	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1<⌈\frac{N}{2}⌉$$
7		elfzo1	$$⊢1\in \left(1..^⌈\frac{N}{2}⌉\right)\leftrightarrow \left(1\in \mathbb{N}\wedge ⌈\frac{N}{2}⌉\in \mathbb{N}\wedge 1<⌈\frac{N}{2}⌉\right)$$
8	2 5 6 7	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in \left(1..^⌈\frac{N}{2}⌉\right)$$