Theorem flcl

Description: The floor (greatest integer) function is an integer (closure law). (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

	Ref	Expression
Assertion	flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$

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		rebtwnz	$$⊢A\in ℝ\to \exists !x\in \mathbb{Z}\left(x\le A\wedge A<x+1\right)$$
3		riotacl	$$⊢\exists !x\in \mathbb{Z}\left(x\le A\wedge A<x+1\right)\to \left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)\in \mathbb{Z}$$
4	2 3	syl	$$⊢A\in ℝ\to \left(\iota x\in \mathbb{Z}|\left(x\le A\wedge A<x+1\right)\right)\in \mathbb{Z}$$
5	1 4	eqeltrd	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$