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