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

Proof

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