Theorem flword2

Description: Ordering relation for the floor function. (Contributed by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Assertion	flword2	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to ⌊B⌋\in {\mathbb{Z}}_{\ge ⌊A⌋}$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to A\in ℝ$$
2	1	flcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to ⌊A⌋\in \mathbb{Z}$$
3		simp2	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to B\in ℝ$$
4	3	flcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to ⌊B⌋\in \mathbb{Z}$$
5		flwordi	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to ⌊A⌋\le ⌊B⌋$$
6		eluz2	$$⊢⌊B⌋\in {\mathbb{Z}}_{\ge ⌊A⌋}\leftrightarrow \left(⌊A⌋\in \mathbb{Z}\wedge ⌊B⌋\in \mathbb{Z}\wedge ⌊A⌋\le ⌊B⌋\right)$$
7	2 4 5 6	syl3anbrc	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to ⌊B⌋\in {\mathbb{Z}}_{\ge ⌊A⌋}$$