Metamath Proof Explorer


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 ( ( 𝐾 ∈ ℕ0𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )

Proof

Step Hyp Ref Expression
1 nn0re ( 𝐾 ∈ ℕ0𝐾 ∈ ℝ )
2 nnrp ( 𝐿 ∈ ℕ → 𝐿 ∈ ℝ+ )
3 fldivle ( ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )
4 1 2 3 syl2an ( ( 𝐾 ∈ ℕ0𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )