Theorem fldivle

Description: The floor function of a division of a real number by a positive real number is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018)

	Ref	Expression
Assertion	fldivle	$$⊢\left(K\in ℝ\wedge L\in {ℝ}^{+}\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	$$⊢\left(K\in ℝ\wedge L\in {ℝ}^{+}\right)\to \frac{K}{L}\in ℝ$$
2		fllelt	$$⊢\frac{K}{L}\in ℝ\to \left(⌊\frac{K}{L}⌋\le \frac{K}{L}\wedge \frac{K}{L}<⌊\frac{K}{L}⌋+1\right)$$
3		simpl	$$⊢\left(⌊\frac{K}{L}⌋\le \frac{K}{L}\wedge \frac{K}{L}<⌊\frac{K}{L}⌋+1\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$
4	1 2 3	3syl	$$⊢\left(K\in ℝ\wedge L\in {ℝ}^{+}\right)\to ⌊\frac{K}{L}⌋\le \frac{K}{L}$$