Description: The floor function of a division of a nonnegative integer by a positive integer is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fldivnn0le | |- ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nn0re | |- ( K e. NN0 -> K e. RR ) |
|
| 2 | nnrp | |- ( L e. NN -> L e. RR+ ) |
|
| 3 | fldivle | |- ( ( K e. RR /\ L e. RR+ ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) ) |
|
| 4 | 1 2 3 | syl2an | |- ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) ) |