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

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+12∈ℝ
5 flltp1 ⊢N+12∈ℝ→N+12<N+12+1
6 4 5 syl ⊢N∈ℤ→N+12<N+12+1
7 4 flcld ⊢N∈ℤ→N+12∈ℤ
8 7 zred ⊢N∈ℤ→N+12∈ℝ
9 1red ⊢N∈ℤ→1∈ℝ
10 8 9 readdcld ⊢N∈ℤ→N+12+1∈ℝ
11 2rp ⊢2∈ℝ+
12 11 a1i ⊢N∈ℤ→2∈ℝ+
13 3 10 12 ltdivmuld ⊢N∈ℤ→N+12<N+12+1↔N+1<2⁢N+12+1
14 6 13 mpbid ⊢N∈ℤ→N+1<2⁢N+12+1
15 9 recnd ⊢N∈ℤ→1∈ℂ
16 15 2timesd ⊢N∈ℤ→2⋅1=1+1
17 16 oveq2d ⊢N∈ℤ→2⁢N+12+2⋅1=2⁢N+12+1+1
18 2cnd ⊢N∈ℤ→2∈ℂ
19 8 recnd ⊢N∈ℤ→N+12∈ℂ
20 18 19 15 adddid ⊢N∈ℤ→2⁢N+12+1=2⁢N+12+2⋅1
21 2re ⊢2∈ℝ
22 21 a1i ⊢N∈ℤ→2∈ℝ
23 22 8 remulcld ⊢N∈ℤ→2⁢N+12∈ℝ
24 23 recnd ⊢N∈ℤ→2⁢N+12∈ℂ
25 24 15 15 addassd ⊢N∈ℤ→2⁢N+12+1+1=2⁢N+12+1+1
26 17 20 25 3eqtr4d ⊢N∈ℤ→2⁢N+12+1=2⁢N+12+1+1
27 14 26 breqtrd ⊢N∈ℤ→N+1<2⁢N+12+1+1
28 23 9 readdcld ⊢N∈ℤ→2⁢N+12+1∈ℝ
29 1 28 9 ltadd1d ⊢N∈ℤ→N<2⁢N+12+1↔N+1<2⁢N+12+1+1
30 27 29 mpbird ⊢N∈ℤ→N<2⁢N+12+1
31 2z ⊢2∈ℤ
32 31 a1i ⊢N∈ℤ→2∈ℤ
33 32 7 zmulcld ⊢N∈ℤ→2⁢N+12∈ℤ
34 zleltp1 ⊢N∈ℤ∧2⁢N+12∈ℤ→N≤2⁢N+12↔N<2⁢N+12+1
35 33 34 mpdan ⊢N∈ℤ→N≤2⁢N+12↔N<2⁢N+12+1
36 30 35 mpbird ⊢N∈ℤ→N≤2⁢N+12