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	⊢ ( 𝑁 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2	1	rehalfcld	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 / 2 ) ∈ ℝ )
3	2	ceilcld	⊢ ( 𝑁 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
4		elnn1uz2	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
5		1le1	⊢ 1 ≤ 1
6		fvoveq1	⊢ ( 𝑁 = 1 → ( ⌈ ‘ ( 𝑁 / 2 ) ) = ( ⌈ ‘ ( 1 / 2 ) ) )
7		ceilhalf1	⊢ ( ⌈ ‘ ( 1 / 2 ) ) = 1
8	6 7	eqtrdi	⊢ ( 𝑁 = 1 → ( ⌈ ‘ ( 𝑁 / 2 ) ) = 1 )
9	5 8	breqtrrid	⊢ ( 𝑁 = 1 → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
10		1red	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
11		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
12	11	rehalfcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ∈ ℝ )
13	12	ceilcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
14	13	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
15		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
16		2re	⊢ 2 ∈ ℝ
17		elicopnf	⊢ ( 2 ∈ ℝ → ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) ) )
18	16 17	ax-mp	⊢ ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) )
19	11 15 18	sylanbrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ( 2 [,) +∞ ) )
20		rehalfge1	⊢ ( 𝑁 ∈ ( 2 [,) +∞ ) → 1 ≤ ( 𝑁 / 2 ) )
21	19 20	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( 𝑁 / 2 ) )
22	12	ceilged	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 / 2 ) ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
23	10 12 14 21 22	letrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
24	9 23	jaoi	⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
25	4 24	sylbi	⊢ ( 𝑁 ∈ ℕ → 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
26		elnnz1	⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ ↔ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
27	3 25 26	sylanbrc	⊢ ( 𝑁 ∈ ℕ → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℕ )