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 {\mathbb{Z}}_{\ge 2}$$
	hashnzfz2.k	$$⊢\phi \to K\in \mathbb{N}$$
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 {\mathbb{Z}}_{\ge 2}$$
2		hashnzfz2.k	$$⊢\phi \to K\in \mathbb{N}$$
3		2nn	$$⊢2\in \mathbb{N}$$
4		uznnssnn	$$⊢2\in \mathbb{N}\to {\mathbb{Z}}_{\ge 2}\subseteq \mathbb{N}$$
5	3 4	ax-mp	$$⊢{\mathbb{Z}}_{\ge 2}\subseteq \mathbb{N}$$
6	5 1	sselid	$$⊢\phi \to N\in \mathbb{N}$$
7		2z	$$⊢2\in \mathbb{Z}$$
8	7	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
9		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
10		2m1e1	$$⊢2-1=1$$
11	10	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(2-1\right)}={\mathbb{Z}}_{\ge 1}$$
12	9 11	eqtr4i	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge \left(2-1\right)}$$
13	2 12	eleqtrdi	$$⊢\phi \to K\in {\mathbb{Z}}_{\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 {\mathbb{Z}}_{\ge 2}\to 2\le N$$
24	1 23	syl	$$⊢\phi \to 2\le N$$
25	6	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
26		zlem1lt	$$⊢\left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(2\le N\leftrightarrow 2-1<N\right)$$
27	7 25 26	sylancr	$$⊢\phi \to \left(2\le N\leftrightarrow 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\leftrightarrow \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 \mathbb{Z}$$
36		flbi	$$⊢\left(\frac{1}{N}\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(⌊\frac{1}{N}⌋=0\leftrightarrow \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\leftrightarrow \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 \mathbb{Z}$$
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}⌋$$