This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flbi

Description: A condition equivalent to floor. (Contributed by NM, 11-Mar-2005) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion flbi ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ B ≤ A ∧ A < B + 1

Proof

Step Hyp Ref Expression
1 flval ⊢ A ∈ ℝ → A = ι x ∈ ℤ | x ≤ A ∧ A < x + 1
2 1 eqeq1d ⊢ A ∈ ℝ → A = B ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = B
3 2 adantr ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = B
4 rebtwnz ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ A < x + 1
5 breq1 ⊢ x = B → x ≤ A ↔ B ≤ A
6 oveq1 ⊢ x = B → x + 1 = B + 1
7 6 breq2d ⊢ x = B → A < x + 1 ↔ A < B + 1
8 5 7 anbi12d ⊢ x = B → x ≤ A ∧ A < x + 1 ↔ B ≤ A ∧ A < B + 1
9 8 riota2 ⊢ B ∈ ℤ ∧ ∃! x ∈ ℤ x ≤ A ∧ A < x + 1 → B ≤ A ∧ A < B + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = B
10 4 9 sylan2 ⊢ B ∈ ℤ ∧ A ∈ ℝ → B ≤ A ∧ A < B + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = B
11 10 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℤ → B ≤ A ∧ A < B + 1 ↔ ι x ∈ ℤ | x ≤ A ∧ A < x + 1 = B
12 3 11 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℤ → A = B ↔ B ≤ A ∧ A < B + 1