Theorem hashnzfz

Description: Special case of hashdvds : the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Hypotheses	hashnzfz.n	$$⊢\phi \to N\in \mathbb{N}$$
	hashnzfz.j	$$⊢\phi \to J\in \mathbb{Z}$$
	hashnzfz.k	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge \left(J-1\right)}$$
Assertion	hashnzfz	$$⊢\phi \to \left|\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)\right|=⌊\frac{K}{N}⌋-⌊\frac{J-1}{N}⌋$$

Proof

Step	Hyp	Ref	Expression
1		hashnzfz.n	$$⊢\phi \to N\in \mathbb{N}$$
2		hashnzfz.j	$$⊢\phi \to J\in \mathbb{Z}$$
3		hashnzfz.k	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge \left(J-1\right)}$$
4		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
5	1 2 3 4	hashdvds	$$⊢\phi \to \left|\left\{x\in \left(J\dots K\right)|N\parallel \left(x-0\right)\right\}\right|=⌊\frac{K-0}{N}⌋-⌊\frac{J-1-0}{N}⌋$$
6		elfzelz	$$⊢x\in \left(J\dots K\right)\to x\in \mathbb{Z}$$
7	6	zcnd	$$⊢x\in \left(J\dots K\right)\to x\in ℂ$$
8	7	subid1d	$$⊢x\in \left(J\dots K\right)\to x-0=x$$
9	8	breq2d	$$⊢x\in \left(J\dots K\right)\to \left(N\parallel \left(x-0\right)\leftrightarrow N\parallel x\right)$$
10	9	rabbiia	$$⊢\left\{x\in \left(J\dots K\right)|N\parallel \left(x-0\right)\right\}=\left\{x\in \left(J\dots K\right)|N\parallel x\right\}$$
11		dfrab3	$$⊢\left\{x\in \left(J\dots K\right)|N\parallel x\right\}=\left(J\dots K\right)\cap \left\{x|N\parallel x\right\}$$
12		reldvds	$$⊢\mathrm{Rel}\parallel$$
13		relimasn	$$⊢\mathrm{Rel}\parallel \to \parallel \left[\left\{N\right\}\right]=\left\{x|N\parallel x\right\}$$
14	12 13	ax-mp	$$⊢\parallel \left[\left\{N\right\}\right]=\left\{x|N\parallel x\right\}$$
15	14	ineq2i	$$⊢\left(J\dots K\right)\cap \parallel \left[\left\{N\right\}\right]=\left(J\dots K\right)\cap \left\{x|N\parallel x\right\}$$
16		incom	$$⊢\left(J\dots K\right)\cap \parallel \left[\left\{N\right\}\right]=\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)$$
17	15 16	eqtr3i	$$⊢\left(J\dots K\right)\cap \left\{x|N\parallel x\right\}=\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)$$
18	10 11 17	3eqtri	$$⊢\left\{x\in \left(J\dots K\right)|N\parallel \left(x-0\right)\right\}=\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)$$
19	18	fveq2i	$$⊢\left|\left\{x\in \left(J\dots K\right)|N\parallel \left(x-0\right)\right\}\right|=\left|\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)\right|$$
20	19	a1i	$$⊢\phi \to \left|\left\{x\in \left(J\dots K\right)|N\parallel \left(x-0\right)\right\}\right|=\left|\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)\right|$$
21		eluzelz	$$⊢K\in {\mathbb{Z}}_{\ge \left(J-1\right)}\to K\in \mathbb{Z}$$
22	3 21	syl	$$⊢\phi \to K\in \mathbb{Z}$$
23	22	zcnd	$$⊢\phi \to K\in ℂ$$
24	23	subid1d	$$⊢\phi \to K-0=K$$
25	24	fvoveq1d	$$⊢\phi \to ⌊\frac{K-0}{N}⌋=⌊\frac{K}{N}⌋$$
26		peano2zm	$$⊢J\in \mathbb{Z}\to J-1\in \mathbb{Z}$$
27	2 26	syl	$$⊢\phi \to J-1\in \mathbb{Z}$$
28	27	zcnd	$$⊢\phi \to J-1\in ℂ$$
29	28	subid1d	$$⊢\phi \to J-1-0=J-1$$
30	29	fvoveq1d	$$⊢\phi \to ⌊\frac{J-1-0}{N}⌋=⌊\frac{J-1}{N}⌋$$
31	25 30	oveq12d	$$⊢\phi \to ⌊\frac{K-0}{N}⌋-⌊\frac{J-1-0}{N}⌋=⌊\frac{K}{N}⌋-⌊\frac{J-1}{N}⌋$$
32	5 20 31	3eqtr3d	$$⊢\phi \to \left|\parallel \left[\left\{N\right\}\right]\cap \left(J\dots K\right)\right|=⌊\frac{K}{N}⌋-⌊\frac{J-1}{N}⌋$$