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	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to (K < N \to ⌊\frac{K}{L}⌋ < \frac{N}{L})$

Proof

Step	Hyp	Ref	Expression
1		nn0nndivcl	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to \frac{K}{L} \in ℝ$
2		reflcl	$⊢ \frac{K}{L} \in ℝ \to ⌊\frac{K}{L}⌋ \in ℝ$
3	1 2	syl	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to ⌊\frac{K}{L}⌋ \in ℝ$
4	3	3adant2	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to ⌊\frac{K}{L}⌋ \in ℝ$
5	1	3adant2	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to \frac{K}{L} \in ℝ$
6		nn0nndivcl	$⊢ (N \in ℕ_{0} \land L \in ℕ) \to \frac{N}{L} \in ℝ$
7	6	3adant1	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to \frac{N}{L} \in ℝ$
8	4 5 7	3jca	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to (⌊\frac{K}{L}⌋ \in ℝ \land \frac{K}{L} \in ℝ \land \frac{N}{L} \in ℝ)$
9	8	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to (⌊\frac{K}{L}⌋ \in ℝ \land \frac{K}{L} \in ℝ \land \frac{N}{L} \in ℝ)$
10		fldivnn0le	$⊢ (K \in ℕ_{0} \land L \in ℕ) \to ⌊\frac{K}{L}⌋ \leq \frac{K}{L}$
11	10	3adant2	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to ⌊\frac{K}{L}⌋ \leq \frac{K}{L}$
12	11	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to ⌊\frac{K}{L}⌋ \leq \frac{K}{L}$
13		simpr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to K < N$
14		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
15		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
16		nnre	$⊢ L \in ℕ \to L \in ℝ$
17		nngt0	$⊢ L \in ℕ \to 0 < L$
18	16 17	jca	$⊢ L \in ℕ \to (L \in ℝ \land 0 < L)$
19	14 15 18	3anim123i	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to (K \in ℝ \land N \in ℝ \land (L \in ℝ \land 0 < L))$
20	19	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to (K \in ℝ \land N \in ℝ \land (L \in ℝ \land 0 < L))$
21		ltdiv1	$⊢ (K \in ℝ \land N \in ℝ \land (L \in ℝ \land 0 < L)) \to (K < N \leftrightarrow \frac{K}{L} < \frac{N}{L})$
22	20 21	syl	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to (K < N \leftrightarrow \frac{K}{L} < \frac{N}{L})$
23	13 22	mpbid	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to \frac{K}{L} < \frac{N}{L}$
24	12 23	jca	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to (⌊\frac{K}{L}⌋ \leq \frac{K}{L} \land \frac{K}{L} < \frac{N}{L})$
25		lelttr	$⊢ (⌊\frac{K}{L}⌋ \in ℝ \land \frac{K}{L} \in ℝ \land \frac{N}{L} \in ℝ) \to ((⌊\frac{K}{L}⌋ \leq \frac{K}{L} \land \frac{K}{L} < \frac{N}{L}) \to ⌊\frac{K}{L}⌋ < \frac{N}{L})$
26	9 24 25	sylc	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \land K < N) \to ⌊\frac{K}{L}⌋ < \frac{N}{L}$
27	26	ex	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land L \in ℕ) \to (K < N \to ⌊\frac{K}{L}⌋ < \frac{N}{L})$

Metamath Proof Explorer

Theorem flltdivnn0lt

Proof