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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renegcl | ||
2 | reflcl | ||
3 | 1 2 | syl | |
4 | flle | ||
5 | 1 4 | syl | |
6 | 5 | adantr | |
7 | lenegcon2 | ||
8 | 6 7 | mpbird | |
9 | 3 8 | mpdan |