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 ) e. RR
2		1re	|- 1 e. RR
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 e. ZZ
11		ceilbi	|- ( ( ( 1 / 2 ) e. RR /\ 1 e. ZZ ) -> ( ( |^ ` ( 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