This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flltdivnn0lt

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

Ref Expression
Assertion flltdivnn0lt ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 < 𝑁 → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝑁 / 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 nn0nndivcl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 / 𝐿 ) ∈ ℝ )
2 reflcl ⊢ ( ( 𝐾 / 𝐿 ) ∈ ℝ → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ )
3 1 2 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ )
4 3 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ )
5 1 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 / 𝐿 ) ∈ ℝ )
6 nn0nndivcl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝑁 / 𝐿 ) ∈ ℝ )
7 6 3adant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝑁 / 𝐿 ) ∈ ℝ )
8 4 5 7 3jca ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ ∧ ( 𝐾 / 𝐿 ) ∈ ℝ ∧ ( 𝑁 / 𝐿 ) ∈ ℝ ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ ∧ ( 𝐾 / 𝐿 ) ∈ ℝ ∧ ( 𝑁 / 𝐿 ) ∈ ℝ ) )
10 fldivnn0le ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )
11 10 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) )
13 simpr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
14 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
15 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
16 nnre ⊢ ( 𝐿 ∈ ℕ → 𝐿 ∈ ℝ )
17 nngt0 ⊢ ( 𝐿 ∈ ℕ → 0 < 𝐿 )
18 16 17 jca ⊢ ( 𝐿 ∈ ℕ → ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) )
19 14 15 18 3anim123i ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) ) )
20 19 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) ) )
21 ltdiv1 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ) ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 / 𝐿 ) < ( 𝑁 / 𝐿 ) ) )
22 20 21 syl ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 / 𝐿 ) < ( 𝑁 / 𝐿 ) ) )
23 13 22 mpbid ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 / 𝐿 ) < ( 𝑁 / 𝐿 ) )
24 12 23 jca ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) ∧ ( 𝐾 / 𝐿 ) < ( 𝑁 / 𝐿 ) ) )
25 lelttr ⊢ ( ( ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ∈ ℝ ∧ ( 𝐾 / 𝐿 ) ∈ ℝ ∧ ( 𝑁 / 𝐿 ) ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) ≤ ( 𝐾 / 𝐿 ) ∧ ( 𝐾 / 𝐿 ) < ( 𝑁 / 𝐿 ) ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝑁 / 𝐿 ) ) )
26 9 24 25 sylc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) ∧ 𝐾 < 𝑁 ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝑁 / 𝐿 ) )
27 26 ex ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ) → ( 𝐾 < 𝑁 → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝑁 / 𝐿 ) ) )