Metamath Proof Explorer


Theorem ceige

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007)

Ref Expression
Assertion ceige A A A

Proof

Step Hyp Ref Expression
1 renegcl A A
2 reflcl A A
3 1 2 syl A A
4 flle A A A
5 1 4 syl A A A
6 5 adantr A A A A
7 lenegcon2 A A A A A A
8 6 7 mpbird A A A A
9 3 8 mpdan A A A