Theorem refldivcl

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

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

Proof

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