Description: Ordering relationship for the greatest integer function. (Contributed by Mario Carneiro, 7-Jun-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | flword2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | ||
2 | 1 | flcld | |
3 | simp2 | ||
4 | 3 | flcld | |
5 | flwordi | ||
6 | eluz2 | ||
7 | 2 4 5 6 | syl3anbrc |