Metamath Proof Explorer

Theorem flge

Description: The floor function value is the greatest integer less than or equal to its argument. (Contributed by NM, 15-Nov-2004) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion flge ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ↔ B ≤ A

Proof

Step Hyp Ref Expression
1 flltp1 ⊢ A ∈ ℝ → A < A + 1
2 1 adantr ⊢ A ∈ ℝ ∧ B ∈ ℤ → A < A + 1
3 simpr ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ∈ ℤ
4 3 zred ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ∈ ℝ
5 simpl ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ∈ ℝ
6 5 flcld ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ∈ ℤ
7 6 peano2zd ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + 1 ∈ ℤ
8 7 zred ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + 1 ∈ ℝ
9 lelttr ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A + 1 ∈ ℝ → B ≤ A ∧ A < A + 1 → B < A + 1
10 4 5 8 9 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ∧ A < A + 1 → B < A + 1
11 2 10 mpan2d ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A → B < A + 1
12 zleltp1 ⊢ B ∈ ℤ ∧ A ∈ ℤ → B ≤ A ↔ B < A + 1
13 3 6 12 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ↔ B < A + 1
14 11 13 sylibrd ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A → B ≤ A
15 flle ⊢ A ∈ ℝ → A ≤ A
16 15 adantr ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ≤ A
17 6 zred ⊢ A ∈ ℝ ∧ B ∈ ℤ → A ∈ ℝ
18 letr ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A ∈ ℝ → B ≤ A ∧ A ≤ A → B ≤ A
19 4 17 5 18 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ∧ A ≤ A → B ≤ A
20 16 19 mpan2d ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A → B ≤ A
21 14 20 impbid ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ↔ B ≤ A