Theorem 2ltceilhalf

Description: The ceiling of half of an integer greater than 2 is greater than or equal to 2. (Contributed by AV, 4-Sep-2025)

	Ref	Expression
Assertion	2ltceilhalf	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uzp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ) )
2		ex-ceil	⊢ ( ( ⌈ ‘ ( 3 / 2 ) ) = 2 ∧ ( ⌈ ‘ - ( 3 / 2 ) ) = - 1 )
3		2re	⊢ 2 ∈ ℝ
4	3	leidi	⊢ 2 ≤ 2
5		breq2	⊢ ( ( ⌈ ‘ ( 3 / 2 ) ) = 2 → ( 2 ≤ ( ⌈ ‘ ( 3 / 2 ) ) ↔ 2 ≤ 2 ) )
6	4 5	mpbiri	⊢ ( ( ⌈ ‘ ( 3 / 2 ) ) = 2 → 2 ≤ ( ⌈ ‘ ( 3 / 2 ) ) )
7	6	adantr	⊢ ( ( ( ⌈ ‘ ( 3 / 2 ) ) = 2 ∧ ( ⌈ ‘ - ( 3 / 2 ) ) = - 1 ) → 2 ≤ ( ⌈ ‘ ( 3 / 2 ) ) )
8	2 7	ax-mp	⊢ 2 ≤ ( ⌈ ‘ ( 3 / 2 ) )
9		fvoveq1	⊢ ( 𝑁 = 3 → ( ⌈ ‘ ( 𝑁 / 2 ) ) = ( ⌈ ‘ ( 3 / 2 ) ) )
10	8 9	breqtrrid	⊢ ( 𝑁 = 3 → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
11	3	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 2 ∈ ℝ )
12		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℝ )
13	12	rehalfcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 / 2 ) ∈ ℝ )
14	13	ceilcld	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
15	14	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
16		2t2e4	⊢ ( 2 · 2 ) = 4
17		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 4 ≤ 𝑁 )
18	16 17	eqbrtrid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 2 ) ≤ 𝑁 )
19		2pos	⊢ 0 < 2
20	3 19	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
21	20	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
22		lemuldiv	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 2 ) ≤ 𝑁 ↔ 2 ≤ ( 𝑁 / 2 ) ) )
23	3 12 21 22	mp3an2i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 2 ) ≤ 𝑁 ↔ 2 ≤ ( 𝑁 / 2 ) ) )
24	18 23	mpbid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 2 ≤ ( 𝑁 / 2 ) )
25	13	ceilged	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 / 2 ) ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
26	11 13 15 24 25	letrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
27		3p1e4	⊢ ( 3 + 1 ) = 4
28	27	fveq2i	⊢ ( ℤ≥ ‘ ( 3 + 1 ) ) = ( ℤ≥ ‘ 4 )
29	26 28	eleq2s	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
30	10 29	jaoi	⊢ ( ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
31	1 30	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )