Theorem ceilhalfnn

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

	Ref	Expression
Assertion	ceilhalfnn	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		nnre	|- ( N e. NN -> N e. RR )
2	1	rehalfcld	|- ( N e. NN -> ( N / 2 ) e. RR )
3	2	ceilcld	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
4		elnn1uz2	|- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
5		1le1	|- 1 <_ 1
6		fvoveq1	|- ( N = 1 -> ( |^ ` ( N / 2 ) ) = ( |^ ` ( 1 / 2 ) ) )
7		ceilhalf1	|- ( |^ ` ( 1 / 2 ) ) = 1
8	6 7	eqtrdi	|- ( N = 1 -> ( |^ ` ( N / 2 ) ) = 1 )
9	5 8	breqtrrid	|- ( N = 1 -> 1 <_ ( |^ ` ( N / 2 ) ) )
10		1red	|- ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
11		eluzelre	|- ( N e. ( ZZ>= ` 2 ) -> N e. RR )
12	11	rehalfcld	|- ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) e. RR )
13	12	ceilcld	|- ( N e. ( ZZ>= ` 2 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
14	13	zred	|- ( N e. ( ZZ>= ` 2 ) -> ( |^ ` ( N / 2 ) ) e. RR )
15		eluzle	|- ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
16		2re	|- 2 e. RR
17		elicopnf	|- ( 2 e. RR -> ( N e. ( 2 [,) +oo ) <-> ( N e. RR /\ 2 <_ N ) ) )
18	16 17	ax-mp	|- ( N e. ( 2 [,) +oo ) <-> ( N e. RR /\ 2 <_ N ) )
19	11 15 18	sylanbrc	|- ( N e. ( ZZ>= ` 2 ) -> N e. ( 2 [,) +oo ) )
20		rehalfge1	|- ( N e. ( 2 [,) +oo ) -> 1 <_ ( N / 2 ) )
21	19 20	syl	|- ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( N / 2 ) )
22	12	ceilged	|- ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) <_ ( |^ ` ( N / 2 ) ) )
23	10 12 14 21 22	letrd	|- ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( |^ ` ( N / 2 ) ) )
24	9 23	jaoi	|- ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> 1 <_ ( |^ ` ( N / 2 ) ) )
25	4 24	sylbi	|- ( N e. NN -> 1 <_ ( |^ ` ( N / 2 ) ) )
26		elnnz1	|- ( ( |^ ` ( N / 2 ) ) e. NN <-> ( ( |^ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |^ ` ( N / 2 ) ) ) )
27	3 25 26	sylanbrc	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) e. NN )