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

Metamath Proof Explorer

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 ℤ$

Proof

Step	Hyp	Ref	Expression
1		flval	$⊢ A \in ℝ \to ⌊A⌋ = (ι x \in ℤ \| (x \leq A \land A < x + 1))$
2		rebtwnz	$⊢ A \in ℝ \to \exists! x \in ℤ (x \leq A \land A < x + 1)$
3		riotacl	$⊢ \exists! x \in ℤ (x \leq A \land A < x + 1) \to (ι x \in ℤ \| (x \leq A \land A < x + 1)) \in ℤ$
4	2 3	syl	$⊢ A \in ℝ \to (ι x \in ℤ \| (x \leq A \land A < x + 1)) \in ℤ$
5	1 4	eqeltrd	$⊢ A \in ℝ \to ⌊A⌋ \in ℤ$