Theorem flltp1

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

	Ref	Expression
Assertion	flltp1	⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		fllelt	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
2	1	simprd	⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )