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 ) ) ) )