Metamath Proof Explorer

Theorem 2ltceilhalf

Description: The ceiling of half of an integer greater than 2 is greater than or equal to 2. (Contributed by AV, 4-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 uzp1 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N = 3 \/ N e. ( ZZ>= ` ( 3 + 1 ) ) ) )
2 ex-ceil 
 |-  ( ( |^ ` ( 3 / 2 ) ) = 2 /\ ( |^ ` -u ( 3 / 2 ) ) = -u 1 )
3 2re 
 |-  2 e. RR
4 3 leidi 
 |-  2 <_ 2
5 breq2 
 |-  ( ( |^ ` ( 3 / 2 ) ) = 2 -> ( 2 <_ ( |^ ` ( 3 / 2 ) ) <-> 2 <_ 2 ) )
6 4 5 mpbiri 
 |-  ( ( |^ ` ( 3 / 2 ) ) = 2 -> 2 <_ ( |^ ` ( 3 / 2 ) ) )
7 6 adantr 
 |-  ( ( ( |^ ` ( 3 / 2 ) ) = 2 /\ ( |^ ` -u ( 3 / 2 ) ) = -u 1 ) -> 2 <_ ( |^ ` ( 3 / 2 ) ) )
8 2 7 ax-mp 
 |-  2 <_ ( |^ ` ( 3 / 2 ) )
9 fvoveq1 
 |-  ( N = 3 -> ( |^ ` ( N / 2 ) ) = ( |^ ` ( 3 / 2 ) ) )
10 8 9 breqtrrid 
 |-  ( N = 3 -> 2 <_ ( |^ ` ( N / 2 ) ) )
11 3 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> 2 e. RR )
12 eluzelre 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. RR )
13 12 rehalfcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N / 2 ) e. RR )
14 13 ceilcld 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( |^ ` ( N / 2 ) ) e. ZZ )
15 14 zred 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( |^ ` ( N / 2 ) ) e. RR )
16 2t2e4 
 |-  ( 2 x. 2 ) = 4
17 eluzle 
 |-  ( N e. ( ZZ>= ` 4 ) -> 4 <_ N )
18 16 17 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 x. 2 ) <_ N )
19 2pos 
 |-  0 < 2
20 3 19 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
21 20 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 e. RR /\ 0 < 2 ) )
22 lemuldiv 
 |-  ( ( 2 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. 2 ) <_ N <-> 2 <_ ( N / 2 ) ) )
23 3 12 21 22 mp3an2i 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 2 x. 2 ) <_ N <-> 2 <_ ( N / 2 ) ) )
24 18 23 mpbid 
 |-  ( N e. ( ZZ>= ` 4 ) -> 2 <_ ( N / 2 ) )
25 13 ceilged 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N / 2 ) <_ ( |^ ` ( N / 2 ) ) )
26 11 13 15 24 25 letrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
27 3p1e4 
 |-  ( 3 + 1 ) = 4
28 27 fveq2i 
 |-  ( ZZ>= ` ( 3 + 1 ) ) = ( ZZ>= ` 4 )
29 26 28 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 3 + 1 ) ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
30 10 29 jaoi 
 |-  ( ( N = 3 \/ N e. ( ZZ>= ` ( 3 + 1 ) ) ) -> 2 <_ ( |^ ` ( N / 2 ) ) )
31 1 30 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 <_ ( |^ ` ( N / 2 ) ) )