Description: The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | fracle1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fraclt1 | |
|
2 | reflcl | |
|
3 | resubcl | |
|
4 | 2 3 | mpdan | |
5 | 1re | |
|
6 | ltle | |
|
7 | 4 5 6 | sylancl | |
8 | 1 7 | mpd | |