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 N 2 N + 1 2

Proof

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