lefldiveq

Description: A closed enough, smaller real C has the same floor of A when both are divided by B . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lefldiveq.a	$⊢ φ \to A \in ℝ$
	lefldiveq.b	$⊢ φ \to B \in ℝ^{+}$
	lefldiveq.c	$⊢ φ \to C \in [A - (A \mod B), A]$
Assertion	lefldiveq	$⊢ φ \to ⌊\frac{A}{B}⌋ = ⌊\frac{C}{B}⌋$

Proof

Step	Hyp	Ref	Expression
1		lefldiveq.a	$⊢ φ \to A \in ℝ$
2		lefldiveq.b	$⊢ φ \to B \in ℝ^{+}$
3		lefldiveq.c	$⊢ φ \to C \in [A - (A \mod B), A]$
4		moddiffl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A - (A \mod B)}{B} = ⌊\frac{A}{B}⌋$
5	1 2 4	syl2anc	$⊢ φ \to \frac{A - (A \mod B)}{B} = ⌊\frac{A}{B}⌋$
6	1 2	rerpdivcld	$⊢ φ \to \frac{A}{B} \in ℝ$
7	6	flcld	$⊢ φ \to ⌊\frac{A}{B}⌋ \in ℤ$
8	5 7	eqeltrd	$⊢ φ \to \frac{A - (A \mod B)}{B} \in ℤ$
9		flid	$⊢ \frac{A - (A \mod B)}{B} \in ℤ \to ⌊\frac{A - (A \mod B)}{B}⌋ = \frac{A - (A \mod B)}{B}$
10	8 9	syl	$⊢ φ \to ⌊\frac{A - (A \mod B)}{B}⌋ = \frac{A - (A \mod B)}{B}$
11	10 5	eqtr2d	$⊢ φ \to ⌊\frac{A}{B}⌋ = ⌊\frac{A - (A \mod B)}{B}⌋$
12	1 2	modcld	$⊢ φ \to A \mod B \in ℝ$
13	1 12	resubcld	$⊢ φ \to A - (A \mod B) \in ℝ$
14	13 2	rerpdivcld	$⊢ φ \to \frac{A - (A \mod B)}{B} \in ℝ$
15		iccssre	$⊢ (A - (A \mod B) \in ℝ \land A \in ℝ) \to [A - (A \mod B), A] \subseteq ℝ$
16	13 1 15	syl2anc	$⊢ φ \to [A - (A \mod B), A] \subseteq ℝ$
17	16 3	sseldd	$⊢ φ \to C \in ℝ$
18	17 2	rerpdivcld	$⊢ φ \to \frac{C}{B} \in ℝ$
19	13	rexrd	$⊢ φ \to A - (A \mod B) \in ℝ^{*}$
20	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
21		iccgelb	$⊢ (A - (A \mod B) \in ℝ^{} \land A \in ℝ^{} \land C \in [A - (A \mod B), A]) \to A - (A \mod B) \leq C$
22	19 20 3 21	syl3anc	$⊢ φ \to A - (A \mod B) \leq C$
23	13 17 2 22	lediv1dd	$⊢ φ \to \frac{A - (A \mod B)}{B} \leq \frac{C}{B}$
24		flwordi	$⊢ (\frac{A - (A \mod B)}{B} \in ℝ \land \frac{C}{B} \in ℝ \land \frac{A - (A \mod B)}{B} \leq \frac{C}{B}) \to ⌊\frac{A - (A \mod B)}{B}⌋ \leq ⌊\frac{C}{B}⌋$
25	14 18 23 24	syl3anc	$⊢ φ \to ⌊\frac{A - (A \mod B)}{B}⌋ \leq ⌊\frac{C}{B}⌋$
26	11 25	eqbrtrd	$⊢ φ \to ⌊\frac{A}{B}⌋ \leq ⌊\frac{C}{B}⌋$
27		iccleub	$⊢ (A - (A \mod B) \in ℝ^{} \land A \in ℝ^{} \land C \in [A - (A \mod B), A]) \to C \leq A$
28	19 20 3 27	syl3anc	$⊢ φ \to C \leq A$
29	17 1 2 28	lediv1dd	$⊢ φ \to \frac{C}{B} \leq \frac{A}{B}$
30		flwordi	$⊢ (\frac{C}{B} \in ℝ \land \frac{A}{B} \in ℝ \land \frac{C}{B} \leq \frac{A}{B}) \to ⌊\frac{C}{B}⌋ \leq ⌊\frac{A}{B}⌋$
31	18 6 29 30	syl3anc	$⊢ φ \to ⌊\frac{C}{B}⌋ \leq ⌊\frac{A}{B}⌋$
32		reflcl	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℝ$
33	6 32	syl	$⊢ φ \to ⌊\frac{A}{B}⌋ \in ℝ$
34		reflcl	$⊢ \frac{C}{B} \in ℝ \to ⌊\frac{C}{B}⌋ \in ℝ$
35	18 34	syl	$⊢ φ \to ⌊\frac{C}{B}⌋ \in ℝ$
36	33 35	letri3d	$⊢ φ \to (⌊\frac{A}{B}⌋ = ⌊\frac{C}{B}⌋ \leftrightarrow (⌊\frac{A}{B}⌋ \leq ⌊\frac{C}{B}⌋ \land ⌊\frac{C}{B}⌋ \leq ⌊\frac{A}{B}⌋))$
37	26 31 36	mpbir2and	$⊢ φ \to ⌊\frac{A}{B}⌋ = ⌊\frac{C}{B}⌋$

Metamath Proof Explorer

Theorem lefldiveq

Proof