Theorem ceilhalfelfzo1

Description: A positive integer less than (the ceiling of) half of another integer is in the half-open range of positive integers up to the other integer. (Contributed by AV, 7-Sep-2025)

	Ref	Expression
Hypothesis	ceilhalfelfzo1.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
Assertion	ceilhalfelfzo1	|- ( N e. NN -> ( K e. J -> K e. ( 1 ..^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		ceilhalfelfzo1.j	|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2	1	eleq2i	|- ( K e. J <-> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )
3		nnre	|- ( N e. NN -> N e. RR )
4	3	rehalfcld	|- ( N e. NN -> ( N / 2 ) e. RR )
5	4	ceilcld	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
6		nnz	|- ( N e. NN -> N e. ZZ )
7		nnnn0	|- ( N e. NN -> N e. NN0 )
8		2nn	|- 2 e. NN
9		nn0ledivnn	|- ( ( N e. NN0 /\ 2 e. NN ) -> ( N / 2 ) <_ N )
10	7 8 9	sylancl	|- ( N e. NN -> ( N / 2 ) <_ N )
11		ceille	|- ( ( ( N / 2 ) e. RR /\ N e. ZZ /\ ( N / 2 ) <_ N ) -> ( |^ ` ( N / 2 ) ) <_ N )
12	4 6 10 11	syl3anc	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) <_ N )
13		eluz2	|- ( N e. ( ZZ>= ` ( |^ ` ( N / 2 ) ) ) <-> ( ( |^ ` ( N / 2 ) ) e. ZZ /\ N e. ZZ /\ ( |^ ` ( N / 2 ) ) <_ N ) )
14	5 6 12 13	syl3anbrc	|- ( N e. NN -> N e. ( ZZ>= ` ( |^ ` ( N / 2 ) ) ) )
15		fzoss2	|- ( N e. ( ZZ>= ` ( |^ ` ( N / 2 ) ) ) -> ( 1 ..^ ( |^ ` ( N / 2 ) ) ) C_ ( 1 ..^ N ) )
16	14 15	syl	|- ( N e. NN -> ( 1 ..^ ( |^ ` ( N / 2 ) ) ) C_ ( 1 ..^ N ) )
17	16	sseld	|- ( N e. NN -> ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) -> K e. ( 1 ..^ N ) ) )
18	2 17	biimtrid	|- ( N e. NN -> ( K e. J -> K e. ( 1 ..^ N ) ) )