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

Metamath Proof Explorer

Theorem flle

Description: A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005)

		Ref	Expression
	Assertion	flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$

Step	Hyp	Ref	Expression
1		fllelt	$⊢ A \in ℝ \to (⌊A⌋ \leq A \land A < ⌊A⌋ + 1)$
2	1	simpld	$⊢ A \in ℝ \to ⌊A⌋ \leq A$