# Metamath Proof Explorer

## Theorem hashnzfz2

Description: Special case of hashnzfz : the count of multiples in nℤ,n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses hashnzfz2.n ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 2}$
hashnzfz2.k ${⊢}{\phi }\to {K}\in ℕ$
Assertion hashnzfz2 ${⊢}{\phi }\to \left|\parallel \left[\left\{{N}\right\}\right]\cap \left(2\dots {K}\right)\right|=⌊\frac{{K}}{{N}}⌋$

### Proof

Step Hyp Ref Expression
1 hashnzfz2.n ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 2}$
2 hashnzfz2.k ${⊢}{\phi }\to {K}\in ℕ$
3 2nn ${⊢}2\in ℕ$
4 uznnssnn ${⊢}2\in ℕ\to {ℤ}_{\ge 2}\subseteq ℕ$
5 3 4 ax-mp ${⊢}{ℤ}_{\ge 2}\subseteq ℕ$
6 5 1 sseldi ${⊢}{\phi }\to {N}\in ℕ$
7 2z ${⊢}2\in ℤ$
8 7 a1i ${⊢}{\phi }\to 2\in ℤ$
9 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
10 2m1e1 ${⊢}2-1=1$
11 10 fveq2i ${⊢}{ℤ}_{\ge \left(2-1\right)}={ℤ}_{\ge 1}$
12 9 11 eqtr4i ${⊢}ℕ={ℤ}_{\ge \left(2-1\right)}$
13 2 12 eleqtrdi ${⊢}{\phi }\to {K}\in {ℤ}_{\ge \left(2-1\right)}$
14 6 8 13 hashnzfz ${⊢}{\phi }\to \left|\parallel \left[\left\{{N}\right\}\right]\cap \left(2\dots {K}\right)\right|=⌊\frac{{K}}{{N}}⌋-⌊\frac{2-1}{{N}}⌋$
15 10 oveq1i ${⊢}\frac{2-1}{{N}}=\frac{1}{{N}}$
16 15 fveq2i ${⊢}⌊\frac{2-1}{{N}}⌋=⌊\frac{1}{{N}}⌋$
17 0red ${⊢}{\phi }\to 0\in ℝ$
18 6 nnrecred ${⊢}{\phi }\to \frac{1}{{N}}\in ℝ$
19 6 nnred ${⊢}{\phi }\to {N}\in ℝ$
20 6 nngt0d ${⊢}{\phi }\to 0<{N}$
21 19 20 recgt0d ${⊢}{\phi }\to 0<\frac{1}{{N}}$
22 17 18 21 ltled ${⊢}{\phi }\to 0\le \frac{1}{{N}}$
23 eluzle ${⊢}{N}\in {ℤ}_{\ge 2}\to 2\le {N}$
24 1 23 syl ${⊢}{\phi }\to 2\le {N}$
25 6 nnzd ${⊢}{\phi }\to {N}\in ℤ$
26 zlem1lt ${⊢}\left(2\in ℤ\wedge {N}\in ℤ\right)\to \left(2\le {N}↔2-1<{N}\right)$
27 7 25 26 sylancr ${⊢}{\phi }\to \left(2\le {N}↔2-1<{N}\right)$
28 24 27 mpbid ${⊢}{\phi }\to 2-1<{N}$
29 10 28 eqbrtrrid ${⊢}{\phi }\to 1<{N}$
30 6 nnrpd ${⊢}{\phi }\to {N}\in {ℝ}^{+}$
31 30 recgt1d ${⊢}{\phi }\to \left(1<{N}↔\frac{1}{{N}}<1\right)$
32 29 31 mpbid ${⊢}{\phi }\to \frac{1}{{N}}<1$
33 0p1e1 ${⊢}0+1=1$
34 32 33 breqtrrdi ${⊢}{\phi }\to \frac{1}{{N}}<0+1$
35 0z ${⊢}0\in ℤ$
36 flbi ${⊢}\left(\frac{1}{{N}}\in ℝ\wedge 0\in ℤ\right)\to \left(⌊\frac{1}{{N}}⌋=0↔\left(0\le \frac{1}{{N}}\wedge \frac{1}{{N}}<0+1\right)\right)$
37 18 35 36 sylancl ${⊢}{\phi }\to \left(⌊\frac{1}{{N}}⌋=0↔\left(0\le \frac{1}{{N}}\wedge \frac{1}{{N}}<0+1\right)\right)$
38 22 34 37 mpbir2and ${⊢}{\phi }\to ⌊\frac{1}{{N}}⌋=0$
39 16 38 syl5eq ${⊢}{\phi }\to ⌊\frac{2-1}{{N}}⌋=0$
40 39 oveq2d ${⊢}{\phi }\to ⌊\frac{{K}}{{N}}⌋-⌊\frac{2-1}{{N}}⌋=⌊\frac{{K}}{{N}}⌋-0$
41 2 nnred ${⊢}{\phi }\to {K}\in ℝ$
42 41 6 nndivred ${⊢}{\phi }\to \frac{{K}}{{N}}\in ℝ$
43 42 flcld ${⊢}{\phi }\to ⌊\frac{{K}}{{N}}⌋\in ℤ$
44 43 zcnd ${⊢}{\phi }\to ⌊\frac{{K}}{{N}}⌋\in ℂ$
45 44 subid1d ${⊢}{\phi }\to ⌊\frac{{K}}{{N}}⌋-0=⌊\frac{{K}}{{N}}⌋$
46 14 40 45 3eqtrd ${⊢}{\phi }\to \left|\parallel \left[\left\{{N}\right\}\right]\cap \left(2\dots {K}\right)\right|=⌊\frac{{K}}{{N}}⌋$