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 ( 𝑁 ∈ ℤ → 𝑁 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑁 + 1 ) / 2 ) ) ) )

Proof

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