Theorem flidm

Description: The floor function is idempotent. (Contributed by NM, 17-Aug-2008)

	Ref	Expression
Assertion	flidm	$$⊢A\in ℝ\to ⌊⌊A⌋⌋=⌊A⌋$$

Proof

Step	Hyp	Ref	Expression
1		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
2		flid	$$⊢⌊A⌋\in \mathbb{Z}\to ⌊⌊A⌋⌋=⌊A⌋$$
3	1 2	syl	$$⊢A\in ℝ\to ⌊⌊A⌋⌋=⌊A⌋$$