Metamath Proof Explorer

Theorem flhalf

Description: Ordering relation for the floor of half of an integer. (Contributed by NM, 1-Jan-2006) (Proof shortened by Mario Carneiro, 7-Jun-2016)

Ref Expression
Assertion flhalf 
|- ( N e. ZZ -> N <_ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
3 1 2 syl 
 |-  ( N e. ZZ -> ( N + 1 ) e. RR )
4 3 rehalfcld 
 |-  ( N e. ZZ -> ( ( N + 1 ) / 2 ) e. RR )
5 flltp1 
 |-  ( ( ( N + 1 ) / 2 ) e. RR -> ( ( N + 1 ) / 2 ) < ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) )
6 4 5 syl 
 |-  ( N e. ZZ -> ( ( N + 1 ) / 2 ) < ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) )
7 4 flcld 
 |-  ( N e. ZZ -> ( |_ ` ( ( N + 1 ) / 2 ) ) e. ZZ )
8 7 zred 
 |-  ( N e. ZZ -> ( |_ ` ( ( N + 1 ) / 2 ) ) e. RR )
9 1red 
 |-  ( N e. ZZ -> 1 e. RR )
10 8 9 readdcld 
 |-  ( N e. ZZ -> ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) e. RR )
11 2rp 
 |-  2 e. RR+
12 11 a1i 
 |-  ( N e. ZZ -> 2 e. RR+ )
13 3 10 12 ltdivmuld 
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) < ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) <-> ( N + 1 ) < ( 2 x. ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) ) ) )
14 6 13 mpbid 
 |-  ( N e. ZZ -> ( N + 1 ) < ( 2 x. ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) ) )
15 9 recnd 
 |-  ( N e. ZZ -> 1 e. CC )
16 15 2timesd 
 |-  ( N e. ZZ -> ( 2 x. 1 ) = ( 1 + 1 ) )
17 16 oveq2d 
 |-  ( N e. ZZ -> ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + ( 2 x. 1 ) ) = ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + ( 1 + 1 ) ) )
18 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
19 8 recnd 
 |-  ( N e. ZZ -> ( |_ ` ( ( N + 1 ) / 2 ) ) e. CC )
20 18 19 15 adddid 
 |-  ( N e. ZZ -> ( 2 x. ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) ) = ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + ( 2 x. 1 ) ) )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( N e. ZZ -> 2 e. RR )
23 22 8 remulcld 
 |-  ( N e. ZZ -> ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) e. RR )
24 23 recnd 
 |-  ( N e. ZZ -> ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) e. CC )
25 24 15 15 addassd 
 |-  ( N e. ZZ -> ( ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) + 1 ) = ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + ( 1 + 1 ) ) )
26 17 20 25 3eqtr4d 
 |-  ( N e. ZZ -> ( 2 x. ( ( |_ ` ( ( N + 1 ) / 2 ) ) + 1 ) ) = ( ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) + 1 ) )
27 14 26 breqtrd 
 |-  ( N e. ZZ -> ( N + 1 ) < ( ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) + 1 ) )
28 23 9 readdcld 
 |-  ( N e. ZZ -> ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) e. RR )
29 1 28 9 ltadd1d 
 |-  ( N e. ZZ -> ( N < ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) <-> ( N + 1 ) < ( ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) + 1 ) ) )
30 27 29 mpbird 
 |-  ( N e. ZZ -> N < ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) )
31 2z 
 |-  2 e. ZZ
32 31 a1i 
 |-  ( N e. ZZ -> 2 e. ZZ )
33 32 7 zmulcld 
 |-  ( N e. ZZ -> ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) e. ZZ )
34 zleltp1 
 |-  ( ( N e. ZZ /\ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) e. ZZ ) -> ( N <_ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) <-> N < ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) ) )
35 33 34 mpdan 
 |-  ( N e. ZZ -> ( N <_ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) <-> N < ( ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) + 1 ) ) )
36 30 35 mpbird 
 |-  ( N e. ZZ -> N <_ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) )