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 A A

Proof

Step Hyp Ref Expression
1 ceige A A A
2 ceilval A A = A
3 1 2 breqtrrd A A A