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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left(⌊{A}⌋={B}↔\left({B}\le {A}\wedge {A}<{B}+1\right)\right)$

Proof

Step Hyp Ref Expression
1 flval ${⊢}{A}\in ℝ\to ⌊{A}⌋=\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
2 1 eqeq1d ${⊢}{A}\in ℝ\to \left(⌊{A}⌋={B}↔\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)={B}\right)$
3 2 adantr ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left(⌊{A}⌋={B}↔\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)={B}\right)$
4 rebtwnz ${⊢}{A}\in ℝ\to \exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)$
5 breq1 ${⊢}{x}={B}\to \left({x}\le {A}↔{B}\le {A}\right)$
6 oveq1 ${⊢}{x}={B}\to {x}+1={B}+1$
7 6 breq2d ${⊢}{x}={B}\to \left({A}<{x}+1↔{A}<{B}+1\right)$
8 5 7 anbi12d ${⊢}{x}={B}\to \left(\left({x}\le {A}\wedge {A}<{x}+1\right)↔\left({B}\le {A}\wedge {A}<{B}+1\right)\right)$
9 8 riota2 ${⊢}\left({B}\in ℤ\wedge \exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)\right)\to \left(\left({B}\le {A}\wedge {A}<{B}+1\right)↔\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)={B}\right)$
10 4 9 sylan2 ${⊢}\left({B}\in ℤ\wedge {A}\in ℝ\right)\to \left(\left({B}\le {A}\wedge {A}<{B}+1\right)↔\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)={B}\right)$
11 10 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left(\left({B}\le {A}\wedge {A}<{B}+1\right)↔\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)={B}\right)$
12 3 11 bitr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℤ\right)\to \left(⌊{A}⌋={B}↔\left({B}\le {A}\wedge {A}<{B}+1\right)\right)$