Theorem ceilhalfnn

Description: The ceiling of half of a positive integer is a positive integer. (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	ceilhalfnn	$$⊢N\in \mathbb{N}\to ⌈\frac{N}{2}⌉\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
2	1	rehalfcld	$$⊢N\in \mathbb{N}\to \frac{N}{2}\in ℝ$$
3	2	ceilcld	$$⊢N\in \mathbb{N}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
4		elnn1uz2	$$⊢N\in \mathbb{N}\leftrightarrow \left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)$$
5		1le1	$$⊢1\le 1$$
6		fvoveq1	$$⊢N=1\to ⌈\frac{N}{2}⌉=⌈\frac{1}{2}⌉$$
7		ceilhalf1	$$⊢⌈\frac{1}{2}⌉=1$$
8	6 7	eqtrdi	$$⊢N=1\to ⌈\frac{N}{2}⌉=1$$
9	5 8	breqtrrid	$$⊢N=1\to 1\le ⌈\frac{N}{2}⌉$$
10		1red	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
11		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℝ$$
12	11	rehalfcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\in ℝ$$
13	12	ceilcld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌈\frac{N}{2}⌉\in \mathbb{Z}$$
14	13	zred	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to ⌈\frac{N}{2}⌉\in ℝ$$
15		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le N$$
16		2re	$$⊢2\in ℝ$$
17		elicopnf	$$⊢2\in ℝ\to \left(N\in \left[2,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 2\le N\right)\right)$$
18	16 17	ax-mp	$$⊢N\in \left[2,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 2\le N\right)$$
19	11 15 18	sylanbrc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \left[2,\mathrm{+\infty }\right)$$
20		rehalfge1	$$⊢N\in \left[2,\mathrm{+\infty }\right)\to 1\le \frac{N}{2}$$
21	19 20	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\le \frac{N}{2}$$
22	12	ceilged	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{N}{2}\le ⌈\frac{N}{2}⌉$$
23	10 12 14 21 22	letrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\le ⌈\frac{N}{2}⌉$$
24	9 23	jaoi	$$⊢\left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)\to 1\le ⌈\frac{N}{2}⌉$$
25	4 24	sylbi	$$⊢N\in \mathbb{N}\to 1\le ⌈\frac{N}{2}⌉$$
26		elnnz1	$$⊢⌈\frac{N}{2}⌉\in \mathbb{N}\leftrightarrow \left(⌈\frac{N}{2}⌉\in \mathbb{Z}\wedge 1\le ⌈\frac{N}{2}⌉\right)$$
27	3 25 26	sylanbrc	$$⊢N\in \mathbb{N}\to ⌈\frac{N}{2}⌉\in \mathbb{N}$$