Theorem ceilhalfgt1

Description: The ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		1red	|- ( N e. ( ZZ>= ` 3 ) -> 1 e. RR )
2		2re	|- 2 e. RR
3	2	a1i	|- ( N e. ( ZZ>= ` 3 ) -> 2 e. RR )
4		eluzelre	|- ( N e. ( ZZ>= ` 3 ) -> N e. RR )
5	4	rehalfcld	|- ( N e. ( ZZ>= ` 3 ) -> ( N / 2 ) e. RR )
6	5	ceilcld	|- ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
7	6	zred	|- ( N e. ( ZZ>= ` 3 ) -> ( |^ ` ( N / 2 ) ) e. RR )
8		1lt2	|- 1 < 2
9	8	a1i	|- ( N e. ( ZZ>= ` 3 ) -> 1 < 2 )
10		2ltceilhalf	|- ( N e. ( ZZ>= ` 3 ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
11	1 3 7 9 10	ltletrd	|- ( N e. ( ZZ>= ` 3 ) -> 1 < ( |^ ` ( N / 2 ) ) )