Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 nn0nndivcl K 0 L K L
2 nn0ge0div K 0 L 0 K L
3 flge0nn0 K L 0 K L K L 0
4 1 2 3 syl2anc K 0 L K L 0