Theorem flle

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

	Ref	Expression
Assertion	flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )

Proof

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