Metamath Proof Explorer

Theorem ceilge

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018)

Ref Expression
Assertion ceilge 
|- ( A e. RR -> A <_ ( |^ ` A ) )

Proof

Step Hyp Ref Expression
1 ceige 
 |-  ( A e. RR -> A <_ -u ( |_ ` -u A ) )
2 ceilval 
 |-  ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
3 1 2 breqtrrd 
 |-  ( A e. RR -> A <_ ( |^ ` A ) )