Theorem 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	$$⊢\phi \to A\in ℝ$$
	lefldiveq.b	$$⊢\phi \to B\in {ℝ}^{+}$$
	lefldiveq.c	$$⊢\phi \to C\in \left[A-\left(A\mathrm{mod}B\right),A\right]$$
Assertion	lefldiveq	$$⊢\phi \to ⌊\frac{A}{B}⌋=⌊\frac{C}{B}⌋$$

Proof

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