Theorem ceilhalf1

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

	Ref	Expression
Assertion	ceilhalf1	⊢ ( ⌈ ‘ ( 1 / 2 ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		halfre	⊢ ( 1 / 2 ) ∈ ℝ
2		1re	⊢ 1 ∈ ℝ
3		halflt1	⊢ ( 1 / 2 ) < 1
4	1 2 3	ltleii	⊢ ( 1 / 2 ) ≤ 1
5		1m1e0	⊢ ( 1 − 1 ) = 0
6		halfgt0	⊢ 0 < ( 1 / 2 )
7	5 6	eqbrtri	⊢ ( 1 − 1 ) < ( 1 / 2 )
8	2 2 1	ltsubaddi	⊢ ( ( 1 − 1 ) < ( 1 / 2 ) ↔ 1 < ( ( 1 / 2 ) + 1 ) )
9	7 8	mpbi	⊢ 1 < ( ( 1 / 2 ) + 1 )
10		1z	⊢ 1 ∈ ℤ
11		ceilbi	⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌈ ‘ ( 1 / 2 ) ) = 1 ↔ ( ( 1 / 2 ) ≤ 1 ∧ 1 < ( ( 1 / 2 ) + 1 ) ) ) )
12	1 10 11	mp2an	⊢ ( ( ⌈ ‘ ( 1 / 2 ) ) = 1 ↔ ( ( 1 / 2 ) ≤ 1 ∧ 1 < ( ( 1 / 2 ) + 1 ) ) )
13	4 9 12	mpbir2an	⊢ ( ⌈ ‘ ( 1 / 2 ) ) = 1