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 NN2N+12

Proof

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