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 \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢y=A\to \left(x\le y\leftrightarrow x\le A\right)$$
2		breq1	$$⊢y=A\to \left(y<x+1\leftrightarrow A<x+1\right)$$
3	1 2	anbi12d	$$⊢y=A\to \left(\left(x\le y\wedge y<x+1\right)\leftrightarrow \left(x\le A\wedge A<x+1\right)\right)$$
4	3	riotabidv	$$⊢y=A\to \left(\iota x\in \mathbb{Z}|\left(x\le y\wedge y<x+1\right)\right)=\left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)$$
5		df-fl	$$⊢⌊.⌋=\left(y\in ℝ⟼\left(\iota x\in \mathbb{Z}|\left(x\le y\wedge y<x+1\right)\right)\right)$$
6		riotaex	$$⊢\left(\iota x\in \mathbb{Z}|\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 \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)$$