Metamath Proof Explorer


Theorem fldivnn0le

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 0 L K L K L

Proof

Step Hyp Ref Expression
1 nn0re K 0 K
2 nnrp L L +
3 fldivle K L + K L K L
4 1 2 3 syl2an K 0 L K L K L