ltmod

Description: A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ltmod.a	$⊢ φ \to A \in ℝ$
	ltmod.b	$⊢ φ \to B \in ℝ^{+}$
	ltmod.c	$⊢ φ \to C \in [A - (A \mod B), A)$
Assertion	ltmod	$⊢ φ \to C \mod B < A \mod B$

Proof

Step	Hyp	Ref	Expression
1		ltmod.a	$⊢ φ \to A \in ℝ$
2		ltmod.b	$⊢ φ \to B \in ℝ^{+}$
3		ltmod.c	$⊢ φ \to C \in [A - (A \mod B), A)$
4	1 2	modcld	$⊢ φ \to A \mod B \in ℝ$
5	1 4	resubcld	$⊢ φ \to A - (A \mod B) \in ℝ$
6	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
7		icossre	$⊢ (A - (A \mod B) \in ℝ \land A \in ℝ^{*}) \to [A - (A \mod B), A) \subseteq ℝ$
8	5 6 7	syl2anc	$⊢ φ \to [A - (A \mod B), A) \subseteq ℝ$
9	8 3	sseldd	$⊢ φ \to C \in ℝ$
10	2	rpred	$⊢ φ \to B \in ℝ$
11	9 2	rerpdivcld	$⊢ φ \to \frac{C}{B} \in ℝ$
12	11	flcld	$⊢ φ \to ⌊\frac{C}{B}⌋ \in ℤ$
13	12	zred	$⊢ φ \to ⌊\frac{C}{B}⌋ \in ℝ$
14	10 13	remulcld	$⊢ φ \to B ⌊\frac{C}{B}⌋ \in ℝ$
15	5	rexrd	$⊢ φ \to A - (A \mod B) \in ℝ^{*}$
16		icoltub	$⊢ (A - (A \mod B) \in ℝ^{} \land A \in ℝ^{} \land C \in [A - (A \mod B), A)) \to C < A$
17	15 6 3 16	syl3anc	$⊢ φ \to C < A$
18	9 1 14 17	ltsub1dd	$⊢ φ \to C - B ⌊\frac{C}{B}⌋ < A - B ⌊\frac{C}{B}⌋$
19		icossicc	$⊢ [A - (A \mod B), A) \subseteq [A - (A \mod B), A]$
20	19 3	sseldi	$⊢ φ \to C \in [A - (A \mod B), A]$
21	1 2 20	lefldiveq	$⊢ φ \to ⌊\frac{A}{B}⌋ = ⌊\frac{C}{B}⌋$
22	21	eqcomd	$⊢ φ \to ⌊\frac{C}{B}⌋ = ⌊\frac{A}{B}⌋$
23	22	oveq2d	$⊢ φ \to B ⌊\frac{C}{B}⌋ = B ⌊\frac{A}{B}⌋$
24	23	oveq2d	$⊢ φ \to A - B ⌊\frac{C}{B}⌋ = A - B ⌊\frac{A}{B}⌋$
25	18 24	breqtrd	$⊢ φ \to C - B ⌊\frac{C}{B}⌋ < A - B ⌊\frac{A}{B}⌋$
26		modval	$⊢ (C \in ℝ \land B \in ℝ^{+}) \to C \mod B = C - B ⌊\frac{C}{B}⌋$
27	9 2 26	syl2anc	$⊢ φ \to C \mod B = C - B ⌊\frac{C}{B}⌋$
28		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
29	1 2 28	syl2anc	$⊢ φ \to A \mod B = A - B ⌊\frac{A}{B}⌋$
30	25 27 29	3brtr4d	$⊢ φ \to C \mod B < A \mod B$

Metamath Proof Explorer

Theorem ltmod

Proof