# Metamath Proof Explorer

## 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 ℕ$
hashnzfz.j ${⊢}{\phi }\to {J}\in ℤ$
hashnzfz.k ${⊢}{\phi }\to {K}\in {ℤ}_{\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 ℕ$
2 hashnzfz.j ${⊢}{\phi }\to {J}\in ℤ$
3 hashnzfz.k ${⊢}{\phi }\to {K}\in {ℤ}_{\ge \left({J}-1\right)}$
4 0zd ${⊢}{\phi }\to 0\in ℤ$
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 ℤ$
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)↔{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 {ℤ}_{\ge \left({J}-1\right)}\to {K}\in ℤ$
22 3 21 syl ${⊢}{\phi }\to {K}\in ℤ$
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 ℤ\to {J}-1\in ℤ$
27 2 26 syl ${⊢}{\phi }\to {J}-1\in ℤ$
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}}⌋$