# 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 ) ) ) )