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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 flval ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) )
2 1 eqeq1d ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = 𝐵 ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = 𝐵 ) )
3 2 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) = 𝐵 ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = 𝐵 ) )
4 rebtwnz ⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) )
5 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ≤ 𝐴 ↔ 𝐵 ≤ 𝐴 ) )
6 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 + 1 ) = ( 𝐵 + 1 ) )
7 6 breq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐴 < ( 𝑥 + 1 ) ↔ 𝐴 < ( 𝐵 + 1 ) ) )
8 5 7 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ↔ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ) )
9 8 riota2 ⊢ ( ( 𝐵 ∈ ℤ ∧ ∃! 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = 𝐵 ) )
10 4 9 sylan2 ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = 𝐵 ) )
11 10 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ↔ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) = 𝐵 ) )
12 3 11 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 𝐵 + 1 ) ) ) )