# Metamath Proof Explorer

## Theorem flval

Description: Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A . (Contributed by NM, 14-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion flval ${⊢}{A}\in ℝ\to ⌊{A}⌋=\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$

### Proof

Step Hyp Ref Expression
1 breq2 ${⊢}{y}={A}\to \left({x}\le {y}↔{x}\le {A}\right)$
2 breq1 ${⊢}{y}={A}\to \left({y}<{x}+1↔{A}<{x}+1\right)$
3 1 2 anbi12d ${⊢}{y}={A}\to \left(\left({x}\le {y}\wedge {y}<{x}+1\right)↔\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
4 3 riotabidv ${⊢}{y}={A}\to \left(\iota {x}\in ℤ|\left({x}\le {y}\wedge {y}<{x}+1\right)\right)=\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
5 df-fl ${⊢}⌊.⌋=\left({y}\in ℝ⟼\left(\iota {x}\in ℤ|\left({x}\le {y}\wedge {y}<{x}+1\right)\right)\right)$
6 riotaex ${⊢}\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)\in \mathrm{V}$
7 4 5 6 fvmpt ${⊢}{A}\in ℝ\to ⌊{A}⌋=\left(\iota {x}\in ℤ|\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$