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 AAA

Proof

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