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 e. RR -> ( |_ ` A ) <_ A )

Proof

Step Hyp Ref Expression
1 fllelt 
 |-  ( A e. RR -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) )
2 1 simpld 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )