Metamath Proof Explorer

Theorem flnn0div2ge

Description: The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020)

Ref Expression
Assertion flnn0div2ge 
|- ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) )

Proof

Step Hyp Ref Expression
1 nn0eo 
 |-  ( N e. NN0 -> ( ( N / 2 ) e. NN0 \/ ( ( N + 1 ) / 2 ) e. NN0 ) )
2 nn0re 
 |-  ( N e. NN0 -> N e. RR )
3 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
4 2 3 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. RR )
5 4 adantl 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> ( N - 1 ) e. RR )
6 2 adantl 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> N e. RR )
7 2rp 
 |-  2 e. RR+
8 7 a1i 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> 2 e. RR+ )
9 2 lem1d 
 |-  ( N e. NN0 -> ( N - 1 ) <_ N )
10 9 adantl 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> ( N - 1 ) <_ N )
11 5 6 8 10 lediv1dd 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> ( ( N - 1 ) / 2 ) <_ ( N / 2 ) )
12 nn0z 
 |-  ( ( N / 2 ) e. NN0 -> ( N / 2 ) e. ZZ )
13 flid 
 |-  ( ( N / 2 ) e. ZZ -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
14 12 13 syl 
 |-  ( ( N / 2 ) e. NN0 -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
15 14 adantr 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
16 11 15 breqtrrd 
 |-  ( ( ( N / 2 ) e. NN0 /\ N e. NN0 ) -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) )
17 16 ex 
 |-  ( ( N / 2 ) e. NN0 -> ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) ) )
18 nn0o 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
19 18 ex 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N - 1 ) / 2 ) e. NN0 ) )
20 nn0z 
 |-  ( ( ( N - 1 ) / 2 ) e. NN0 -> ( ( N - 1 ) / 2 ) e. ZZ )
21 20 adantl 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. ZZ )
22 flid 
 |-  ( ( ( N - 1 ) / 2 ) e. ZZ -> ( |_ ` ( ( N - 1 ) / 2 ) ) = ( ( N - 1 ) / 2 ) )
23 21 22 syl 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( ( N - 1 ) / 2 ) ) = ( ( N - 1 ) / 2 ) )
24 4 rehalfcld 
 |-  ( N e. NN0 -> ( ( N - 1 ) / 2 ) e. RR )
25 24 adantr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. RR )
26 2 rehalfcld 
 |-  ( N e. NN0 -> ( N / 2 ) e. RR )
27 26 adantr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( N / 2 ) e. RR )
28 2re 
 |-  2 e. RR
29 2pos 
 |-  0 < 2
30 28 29 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
31 30 a1i 
 |-  ( N e. NN0 -> ( 2 e. RR /\ 0 < 2 ) )
32 lediv1 
 |-  ( ( ( N - 1 ) e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( N - 1 ) <_ N <-> ( ( N - 1 ) / 2 ) <_ ( N / 2 ) ) )
33 4 2 31 32 syl3anc 
 |-  ( N e. NN0 -> ( ( N - 1 ) <_ N <-> ( ( N - 1 ) / 2 ) <_ ( N / 2 ) ) )
34 9 33 mpbid 
 |-  ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( N / 2 ) )
35 34 adantr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) <_ ( N / 2 ) )
36 flwordi 
 |-  ( ( ( ( N - 1 ) / 2 ) e. RR /\ ( N / 2 ) e. RR /\ ( ( N - 1 ) / 2 ) <_ ( N / 2 ) ) -> ( |_ ` ( ( N - 1 ) / 2 ) ) <_ ( |_ ` ( N / 2 ) ) )
37 25 27 35 36 syl3anc 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( ( N - 1 ) / 2 ) ) <_ ( |_ ` ( N / 2 ) ) )
38 23 37 eqbrtrrd 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) )
39 38 ex 
 |-  ( N e. NN0 -> ( ( ( N - 1 ) / 2 ) e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) ) )
40 19 39 syldc 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) ) )
41 17 40 jaoi 
 |-  ( ( ( N / 2 ) e. NN0 \/ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) ) )
42 1 41 mpcom 
 |-  ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) )