Description: The floor (greatest integer) function is an integer (closure law). (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | flcl | |- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | flval | |- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) ) |
|
| 2 | rebtwnz | |- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) |
|
| 3 | riotacl | |- ( E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) -> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) e. ZZ ) |
|
| 4 | 2 3 | syl | |- ( A e. RR -> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) e. ZZ ) |
| 5 | 1 4 | eqeltrd | |- ( A e. RR -> ( |_ ` A ) e. ZZ ) |