Theorem ceilhalf1

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

	Ref	Expression
Assertion	ceilhalf1	$$⊢⌈\frac{1}{2}⌉=1$$

Proof

Step	Hyp	Ref	Expression
1		halfre	$$⊢\frac{1}{2}\in ℝ$$
2		1re	$$⊢1\in ℝ$$
3		halflt1	$$⊢\frac{1}{2}<1$$
4	1 2 3	ltleii	$$⊢\frac{1}{2}\le 1$$
5		1m1e0	$$⊢1-1=0$$
6		halfgt0	$$⊢0<\frac{1}{2}$$
7	5 6	eqbrtri	$$⊢1-1<\frac{1}{2}$$
8	2 2 1	ltsubaddi	$$⊢1-1<\frac{1}{2}\leftrightarrow 1<\left(\frac{1}{2}\right)+1$$
9	7 8	mpbi	$$⊢1<\left(\frac{1}{2}\right)+1$$
10		1z	$$⊢1\in \mathbb{Z}$$
11		ceilbi	$$⊢\left(\frac{1}{2}\in ℝ\wedge 1\in \mathbb{Z}\right)\to \left(⌈\frac{1}{2}⌉=1\leftrightarrow \left(\frac{1}{2}\le 1\wedge 1<\left(\frac{1}{2}\right)+1\right)\right)$$
12	1 10 11	mp2an	$$⊢⌈\frac{1}{2}⌉=1\leftrightarrow \left(\frac{1}{2}\le 1\wedge 1<\left(\frac{1}{2}\right)+1\right)$$
13	4 9 12	mpbir2an	$$⊢⌈\frac{1}{2}⌉=1$$