Metamath Proof Explorer

Theorem flword2

Description: Ordering relationship for the greatest integer function. (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Assertion flword2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℤ ≥ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℝ
2 1 flcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℤ
3 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℝ
4 3 flcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℤ
5 flwordi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B
6 eluz2 ⊢ B ∈ ℤ ≥ A ↔ A ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B
7 2 4 5 6 syl3anbrc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℤ ≥ A