Theorem flidm

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

	Ref	Expression
Assertion	flidm	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		flcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
2		flid	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )