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	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢K\in {\mathbb{N}}_0\to K\in ℝ$$
2		nnrp	$$⊢L\in \mathbb{N}\to L\in {ℝ}^{+}$$
3		fldivle	$$⊢\left(K\in ℝ\wedge L\in {ℝ}^{+}\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$
4	1 2 3	syl2an	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$