Theorem fldivnn0

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

	Ref	Expression
Assertion	fldivnn0	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to ⌊\frac{K}{L}⌋\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nn0nndivcl	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to \frac{K}{L}\in ℝ$$
2		nn0ge0div	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to 0\le \frac{K}{L}$$
3		flge0nn0	$$⊢\left(\frac{K}{L}\in ℝ\wedge 0\le \frac{K}{L}\right)\to ⌊\frac{K}{L}⌋\in {\mathbb{N}}_0$$
4	1 2 3	syl2anc	$$⊢\left(K\in {\mathbb{N}}_0\wedge L\in \mathbb{N}\right)\to ⌊\frac{K}{L}⌋\in {\mathbb{N}}_0$$