Theorem fllelt

Description: A basic property of the floor (greatest integer) function. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

	Ref	Expression
Assertion	fllelt	$$⊢A\in ℝ\to \left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		flval	$$⊢A\in ℝ\to ⌊A⌋=\left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)$$
2	1	eqcomd	$$⊢A\in ℝ\to \left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)=⌊A⌋$$
3		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
4		rebtwnz	$$⊢A\in ℝ\to \exists !x\in \mathbb{Z}\left(x\le A\wedge A<x+1\right)$$
5		breq1	$$⊢x=⌊A⌋\to \left(x\le A\leftrightarrow ⌊A⌋\le A\right)$$
6		oveq1	$$⊢x=⌊A⌋\to x+1=⌊A⌋+1$$
7	6	breq2d	$$⊢x=⌊A⌋\to \left(A<x+1\leftrightarrow A<⌊A⌋+1\right)$$
8	5 7	anbi12d	$$⊢x=⌊A⌋\to \left(\left(x\le A\wedge A<x+1\right)\leftrightarrow \left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)\right)$$
9	8	riota2	$$⊢\left(⌊A⌋\in \mathbb{Z}\wedge \exists !x\in \mathbb{Z}\left(x\le A\wedge A<x+1\right)\right)\to \left(\left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)\leftrightarrow \left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)=⌊A⌋\right)$$
10	3 4 9	syl2anc	$$⊢A\in ℝ\to \left(\left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)\leftrightarrow \left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)=⌊A⌋\right)$$
11	2 10	mpbird	$$⊢A\in ℝ\to \left(⌊A⌋\le A\wedge A<⌊A⌋+1\right)$$