flword2

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

		Ref	Expression
	Assertion	flword2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ⌊B⌋ \in ℤ_{\geq ⌊A⌋}$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \in ℝ$
2	1	flcld	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ⌊A⌋ \in ℤ$
3		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B \in ℝ$
4	3	flcld	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ⌊B⌋ \in ℤ$
5		flwordi	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ⌊A⌋ \leq ⌊B⌋$
6		eluz2	$⊢ ⌊B⌋ \in ℤ_{\geq ⌊A⌋} \leftrightarrow (⌊A⌋ \in ℤ \land ⌊B⌋ \in ℤ \land ⌊A⌋ \leq ⌊B⌋)$
7	2 4 5 6	syl3anbrc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to ⌊B⌋ \in ℤ_{\geq ⌊A⌋}$

Metamath Proof Explorer