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

Metamath Proof Explorer

Theorem flltp1

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

		Ref	Expression
	Assertion	flltp1	$⊢ A \in ℝ \to A < ⌊A⌋ + 1$

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