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