Metamath Proof Explorer

Theorem fllelt

Description: A basic property of the floor (greatest integer) function. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion fllelt ⊢ A ∈ ℝ → A ≤ A ∧ A < A + 1

Proof

Step Hyp Ref Expression
1 flval ⊢ A ∈ ℝ → A = ι x ∈ ℤ | x ≤ A ∧ A < x + 1
2 1 eqcomd ⊢ A ∈ ℝ → ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = A
3 flcl ⊢ A ∈ ℝ → A ∈ ℤ
4 rebtwnz ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ A < x + 1
5 breq1 ⊢ x = A → x ≤ A ↔ A ≤ A
6 oveq1 ⊢ x = A → x + 1 = A + 1
7 6 breq2d ⊢ x = A → A < x + 1 ↔ A < A + 1
8 5 7 anbi12d ⊢ x = A → x ≤ A ∧ A < x + 1 ↔ A ≤ A ∧ A < A + 1
9 8 riota2 ⊢ A ∈ ℤ ∧ ∃! x ∈ ℤ x ≤ A ∧ A < x + 1 → A ≤ A ∧ A < A + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = A
10 3 4 9 syl2anc ⊢ A ∈ ℝ → A ≤ A ∧ A < A + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = A
11 2 10 mpbird ⊢ A ∈ ℝ → A ≤ A ∧ A < A + 1