Metamath Proof Explorer

Theorem flwordi

Description: Ordering relationship for the greatest integer function. (Contributed by NM, 31-Dec-2005) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion flwordi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℝ
2 1 flcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℤ
3 2 zred ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℝ
4 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℝ
5 flle ⊢ A ∈ ℝ → A ≤ A
6 1 5 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ A
7 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B
8 3 1 4 6 7 letrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B
9 flge ⊢ B ∈ ℝ ∧ A ∈ ℤ → A ≤ B ↔ A ≤ B
10 4 2 9 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B ↔ A ≤ B
11 8 10 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B