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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( ⌈ ‘ ( 𝑁 / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1red	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℝ )
2		2re	⊢ 2 ∈ ℝ
3	2	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ )
4		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
5	4	rehalfcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 / 2 ) ∈ ℝ )
6	5	ceilcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
7	6	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
8		1lt2	⊢ 1 < 2
9	8	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < 2 )
10		2ltceilhalf	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
11	1 3 7 9 10	ltletrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( ⌈ ‘ ( 𝑁 / 2 ) ) )