This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flidm

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

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

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