Theorem 1elfzo1ceilhalf1

Description: 1 is in the half-open integer range from 1 to the ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025)

	Ref	Expression
Assertion	1elfzo1ceilhalf1	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		1nn	|- 1 e. NN
2	1	a1i	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. NN )
3		eluzge3nn	|- ( N e. ( ZZ>= ` 3 ) -> N e. NN )
4		ceilhalfnn	|- ( N e. NN -> ( |^ ` ( N / 2 ) ) e. NN )
5	3 4	syl	|- ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. NN )
6		ceilhalfgt1	|- ( N e. ( ZZ>= ` 3 ) -> 1 < ( |^ ` ( N / 2 ) ) )
7		elfzo1	|- ( 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( 1 e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ 1 < ( |^ ` ( N / 2 ) ) ) )
8	2 5 6 7	syl3anbrc	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )