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