Description: A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | ceilidz | |- ( A e. RR -> ( A e. ZZ <-> ( |^ ` A ) = A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceilid | |- ( A e. ZZ -> ( |^ ` A ) = A ) |
|
2 | ceilcl | |- ( A e. RR -> ( |^ ` A ) e. ZZ ) |
|
3 | eleq1 | |- ( ( |^ ` A ) = A -> ( ( |^ ` A ) e. ZZ <-> A e. ZZ ) ) |
|
4 | 2 3 | syl5ibcom | |- ( A e. RR -> ( ( |^ ` A ) = A -> A e. ZZ ) ) |
5 | 1 4 | impbid2 | |- ( A e. RR -> ( A e. ZZ <-> ( |^ ` A ) = A ) ) |