# Metamath Proof Explorer

## Theorem hashnzfzclim

Description: As the upper bound K of the constraint interval ( J ... K ) in hashnzfz increases, the resulting count of multiples tends to ( K / M ) —that is, there are approximately ( K / M ) multiples of M in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses hashnzfzclim.m ${⊢}{\phi }\to {M}\in ℕ$
hashnzfzclim.j ${⊢}{\phi }\to {J}\in ℤ$
Assertion hashnzfzclim ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{\left|\parallel \left[\left\{{M}\right\}\right]\cap \left({J}\dots {k}\right)\right|}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$

### Proof

Step Hyp Ref Expression
1 hashnzfzclim.m ${⊢}{\phi }\to {M}\in ℕ$
2 hashnzfzclim.j ${⊢}{\phi }\to {J}\in ℤ$
3 1 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({J}-1\right)}\right)\to {M}\in ℕ$
4 2 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({J}-1\right)}\right)\to {J}\in ℤ$
5 simpr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({J}-1\right)}\right)\to {k}\in {ℤ}_{\ge \left({J}-1\right)}$
6 3 4 5 hashnzfz ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({J}-1\right)}\right)\to \left|\parallel \left[\left\{{M}\right\}\right]\cap \left({J}\dots {k}\right)\right|=⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋$
7 6 oveq1d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({J}-1\right)}\right)\to \frac{\left|\parallel \left[\left\{{M}\right\}\right]\cap \left({J}\dots {k}\right)\right|}{{k}}=\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}$
8 7 mpteq2dva ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{\left|\parallel \left[\left\{{M}\right\}\right]\cap \left({J}\dots {k}\right)\right|}{{k}}\right)=\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
9 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
10 1z ${⊢}1\in ℤ$
11 10 a1i ${⊢}{\phi }\to 1\in ℤ$
12 1 nncnd ${⊢}{\phi }\to {M}\in ℂ$
13 1 nnne0d ${⊢}{\phi }\to {M}\ne 0$
14 12 13 reccld ${⊢}{\phi }\to \frac{1}{{M}}\in ℂ$
15 9 eqimss2i ${⊢}{ℤ}_{\ge 1}\subseteq ℕ$
16 nnex ${⊢}ℕ\in \mathrm{V}$
17 15 16 climconst2 ${⊢}\left(\frac{1}{{M}}\in ℂ\wedge 1\in ℤ\right)\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)⇝\left(\frac{1}{{M}}\right)$
18 14 10 17 sylancl ${⊢}{\phi }\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)⇝\left(\frac{1}{{M}}\right)$
19 16 mptex ${⊢}\left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\in \mathrm{V}$
20 19 a1i ${⊢}{\phi }\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\in \mathrm{V}$
21 ax-1cn ${⊢}1\in ℂ$
22 divcnv ${⊢}1\in ℂ\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)⇝0$
23 21 22 mp1i ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)⇝0$
24 ovex ${⊢}\frac{1}{{M}}\in \mathrm{V}$
25 24 fvconst2 ${⊢}{x}\in ℕ\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)\left({x}\right)=\frac{1}{{M}}$
26 25 adantl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)\left({x}\right)=\frac{1}{{M}}$
27 14 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{1}{{M}}\in ℂ$
28 26 27 eqeltrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)\left({x}\right)\in ℂ$
29 eqidd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)=\left({k}\in ℕ⟼\frac{1}{{k}}\right)$
30 oveq2 ${⊢}{k}={x}\to \frac{1}{{k}}=\frac{1}{{x}}$
31 30 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \frac{1}{{k}}=\frac{1}{{x}}$
32 simpr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {x}\in ℕ$
33 ovexd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{1}{{x}}\in \mathrm{V}$
34 29 31 32 33 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)\left({x}\right)=\frac{1}{{x}}$
35 32 nnrecred ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{1}{{x}}\in ℝ$
36 34 35 eqeltrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)\left({x}\right)\in ℝ$
37 36 recnd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{1}{{k}}\right)\left({x}\right)\in ℂ$
38 eqidd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)=\left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)$
39 30 oveq2d ${⊢}{k}={x}\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
40 39 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
41 ovexd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)\in \mathrm{V}$
42 38 40 32 41 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\left({x}\right)=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
43 26 34 oveq12d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(ℕ×\left\{\frac{1}{{M}}\right\}\right)\left({x}\right)-\left({k}\in ℕ⟼\frac{1}{{k}}\right)\left({x}\right)=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
44 42 43 eqtr4d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\left({x}\right)=\left(ℕ×\left\{\frac{1}{{M}}\right\}\right)\left({x}\right)-\left({k}\in ℕ⟼\frac{1}{{k}}\right)\left({x}\right)$
45 9 11 18 20 23 28 37 44 climsub ${⊢}{\phi }\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)⇝\left(\left(\frac{1}{{M}}\right)-0\right)$
46 14 subid1d ${⊢}{\phi }\to \left(\frac{1}{{M}}\right)-0=\frac{1}{{M}}$
47 45 46 breqtrd ${⊢}{\phi }\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)⇝\left(\frac{1}{{M}}\right)$
48 16 mptex ${⊢}\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\in \mathrm{V}$
49 48 a1i ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\in \mathrm{V}$
50 1 nnrecred ${⊢}{\phi }\to \frac{1}{{M}}\in ℝ$
51 50 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{1}{{M}}\in ℝ$
52 nnre ${⊢}{x}\in ℕ\to {x}\in ℝ$
53 52 adantl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {x}\in ℝ$
54 nnne0 ${⊢}{x}\in ℕ\to {x}\ne 0$
55 54 adantl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {x}\ne 0$
56 53 55 rereccld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{1}{{x}}\in ℝ$
57 51 56 resubcld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)\in ℝ$
58 42 57 eqeltrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\left({x}\right)\in ℝ$
59 eqidd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)=\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)$
60 fvoveq1 ${⊢}{k}={x}\to ⌊\frac{{k}}{{M}}⌋=⌊\frac{{x}}{{M}}⌋$
61 id ${⊢}{k}={x}\to {k}={x}$
62 60 61 oveq12d ${⊢}{k}={x}\to \frac{⌊\frac{{k}}{{M}}⌋}{{k}}=\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
63 62 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \frac{⌊\frac{{k}}{{M}}⌋}{{k}}=\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
64 ovexd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋}{{x}}\in \mathrm{V}$
65 59 63 32 64 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)=\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
66 1 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {M}\in ℕ$
67 53 66 nndivred ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{{x}}{{M}}\in ℝ$
68 reflcl ${⊢}\frac{{x}}{{M}}\in ℝ\to ⌊\frac{{x}}{{M}}⌋\in ℝ$
69 67 68 syl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{x}}{{M}}⌋\in ℝ$
70 69 53 55 redivcld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋}{{x}}\in ℝ$
71 65 70 eqeltrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)\in ℝ$
72 67 recnd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{{x}}{{M}}\in ℂ$
73 1cnd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to 1\in ℂ$
74 nncn ${⊢}{x}\in ℕ\to {x}\in ℂ$
75 74 adantl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {x}\in ℂ$
76 72 73 75 55 divsubdird ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{\left(\frac{{x}}{{M}}\right)-1}{{x}}=\left(\frac{\frac{{x}}{{M}}}{{x}}\right)-\left(\frac{1}{{x}}\right)$
77 12 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {M}\in ℂ$
78 13 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {M}\ne 0$
79 75 77 78 divrecd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{{x}}{{M}}={x}\left(\frac{1}{{M}}\right)$
80 79 oveq1d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{\frac{{x}}{{M}}}{{x}}=\frac{{x}\left(\frac{1}{{M}}\right)}{{x}}$
81 27 75 55 divcan3d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{{x}\left(\frac{1}{{M}}\right)}{{x}}=\frac{1}{{M}}$
82 80 81 eqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{\frac{{x}}{{M}}}{{x}}=\frac{1}{{M}}$
83 82 oveq1d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{\frac{{x}}{{M}}}{{x}}\right)-\left(\frac{1}{{x}}\right)=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
84 76 83 eqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{\left(\frac{{x}}{{M}}\right)-1}{{x}}=\left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)$
85 1red ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to 1\in ℝ$
86 67 85 resubcld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{{x}}{{M}}\right)-1\in ℝ$
87 nnrp ${⊢}{x}\in ℕ\to {x}\in {ℝ}^{+}$
88 87 adantl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to {x}\in {ℝ}^{+}$
89 69 85 readdcld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{x}}{{M}}⌋+1\in ℝ$
90 flle ${⊢}\frac{{x}}{{M}}\in ℝ\to ⌊\frac{{x}}{{M}}⌋\le \frac{{x}}{{M}}$
91 67 90 syl ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{x}}{{M}}⌋\le \frac{{x}}{{M}}$
92 flflp1 ${⊢}\left(\frac{{x}}{{M}}\in ℝ\wedge \frac{{x}}{{M}}\in ℝ\right)\to \left(⌊\frac{{x}}{{M}}⌋\le \frac{{x}}{{M}}↔\frac{{x}}{{M}}<⌊\frac{{x}}{{M}}⌋+1\right)$
93 67 67 92 syl2anc ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(⌊\frac{{x}}{{M}}⌋\le \frac{{x}}{{M}}↔\frac{{x}}{{M}}<⌊\frac{{x}}{{M}}⌋+1\right)$
94 91 93 mpbid ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{{x}}{{M}}<⌊\frac{{x}}{{M}}⌋+1$
95 67 89 85 94 ltsub1dd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{{x}}{{M}}\right)-1<⌊\frac{{x}}{{M}}⌋+1-1$
96 69 recnd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{x}}{{M}}⌋\in ℂ$
97 96 73 pncand ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{x}}{{M}}⌋+1-1=⌊\frac{{x}}{{M}}⌋$
98 95 97 breqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{{x}}{{M}}\right)-1<⌊\frac{{x}}{{M}}⌋$
99 86 69 88 98 ltdiv1dd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{\left(\frac{{x}}{{M}}\right)-1}{{x}}<\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
100 84 99 eqbrtrrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)<\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
101 57 70 100 ltled ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left(\frac{1}{{M}}\right)-\left(\frac{1}{{x}}\right)\le \frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
102 simpr ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to {k}={x}$
103 102 fvoveq1d ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to ⌊\frac{{k}}{{M}}⌋=⌊\frac{{x}}{{M}}⌋$
104 103 102 oveq12d ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \frac{⌊\frac{{k}}{{M}}⌋}{{k}}=\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
105 59 104 32 64 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)=\frac{⌊\frac{{x}}{{M}}⌋}{{x}}$
106 101 42 105 3brtr4d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\left(\frac{1}{{M}}\right)-\left(\frac{1}{{k}}\right)\right)\left({x}\right)\le \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)$
107 69 67 88 91 lediv1dd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋}{{x}}\le \frac{\frac{{x}}{{M}}}{{x}}$
108 107 82 breqtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋}{{x}}\le \frac{1}{{M}}$
109 105 108 eqbrtrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)\le \frac{1}{{M}}$
110 9 11 47 49 58 71 106 109 climsqz ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
111 16 mptex ${⊢}\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\in \mathrm{V}$
112 111 a1i ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\in \mathrm{V}$
113 2 zred ${⊢}{\phi }\to {J}\in ℝ$
114 1red ${⊢}{\phi }\to 1\in ℝ$
115 113 114 resubcld ${⊢}{\phi }\to {J}-1\in ℝ$
116 115 1 nndivred ${⊢}{\phi }\to \frac{{J}-1}{{M}}\in ℝ$
117 116 flcld ${⊢}{\phi }\to ⌊\frac{{J}-1}{{M}}⌋\in ℤ$
118 117 zcnd ${⊢}{\phi }\to ⌊\frac{{J}-1}{{M}}⌋\in ℂ$
119 divcnv ${⊢}⌊\frac{{J}-1}{{M}}⌋\in ℂ\to \left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝0$
120 118 119 syl ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝0$
121 71 recnd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)\in ℂ$
122 eqidd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)=\left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
123 oveq2 ${⊢}{k}={x}\to \frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}=\frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}$
124 123 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}=\frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}$
125 ovexd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}\in \mathrm{V}$
126 122 124 32 125 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)=\frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}$
127 118 adantr ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to ⌊\frac{{J}-1}{{M}}⌋\in ℂ$
128 127 75 55 divcld ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}\in ℂ$
129 126 128 eqeltrd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)\in ℂ$
130 96 127 75 55 divsubdird ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{x}}=\left(\frac{⌊\frac{{x}}{{M}}⌋}{{x}}\right)-\left(\frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}\right)$
131 eqidd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)=\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
132 60 oveq1d ${⊢}{k}={x}\to ⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋=⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋$
133 132 61 oveq12d ${⊢}{k}={x}\to \frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}=\frac{⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{x}}$
134 133 adantl ${⊢}\left(\left({\phi }\wedge {x}\in ℕ\right)\wedge {k}={x}\right)\to \frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}=\frac{⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{x}}$
135 ovexd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \frac{⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{x}}\in \mathrm{V}$
136 131 134 32 135 fvmptd ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)=\frac{⌊\frac{{x}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{x}}$
137 65 126 oveq12d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)-\left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)=\left(\frac{⌊\frac{{x}}{{M}}⌋}{{x}}\right)-\left(\frac{⌊\frac{{J}-1}{{M}}⌋}{{x}}\right)$
138 130 136 137 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in ℕ\right)\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)=\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋}{{k}}\right)\left({x}\right)-\left({k}\in ℕ⟼\frac{⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\left({x}\right)$
139 9 11 110 112 120 121 129 138 climsub ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\left(\frac{1}{{M}}\right)-0\right)$
140 139 46 breqtrd ${⊢}{\phi }\to \left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
141 uzssz ${⊢}{ℤ}_{\ge \left({J}-1\right)}\subseteq ℤ$
142 resmpt ${⊢}{ℤ}_{\ge \left({J}-1\right)}\subseteq ℤ\to {\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge \left({J}-1\right)}}=\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
143 141 142 ax-mp ${⊢}{\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge \left({J}-1\right)}}=\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
144 143 breq1i ${⊢}\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge \left({J}-1\right)}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
145 2 11 zsubcld ${⊢}{\phi }\to {J}-1\in ℤ$
146 zex ${⊢}ℤ\in \mathrm{V}$
147 146 mptex ${⊢}\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\in \mathrm{V}$
148 climres ${⊢}\left({J}-1\in ℤ\wedge \left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\in \mathrm{V}\right)\to \left(\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge \left({J}-1\right)}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)\right)$
149 145 147 148 sylancl ${⊢}{\phi }\to \left(\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge \left({J}-1\right)}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)\right)$
150 144 149 syl5bbr ${⊢}{\phi }\to \left(\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)\right)$
151 9 reseq2i ${⊢}{\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{ℕ}={\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge 1}}$
152 151 breq1i ${⊢}\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{ℕ}\right)⇝\left(\frac{1}{{M}}\right)↔\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge 1}}\right)⇝\left(\frac{1}{{M}}\right)$
153 nnssz ${⊢}ℕ\subseteq ℤ$
154 resmpt ${⊢}ℕ\subseteq ℤ\to {\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{ℕ}=\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
155 153 154 ax-mp ${⊢}{\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{ℕ}=\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)$
156 155 breq1i ${⊢}\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{ℕ}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
157 climres ${⊢}\left(1\in ℤ\wedge \left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)\in \mathrm{V}\right)\to \left(\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge 1}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)\right)$
158 10 147 157 mp2an ${⊢}\left({\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)↾}_{{ℤ}_{\ge 1}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
159 152 156 158 3bitr3i ${⊢}\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℤ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
160 150 159 syl6bbr ${⊢}{\phi }\to \left(\left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)↔\left({k}\in ℕ⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)\right)$
161 140 160 mpbird ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{⌊\frac{{k}}{{M}}⌋-⌊\frac{{J}-1}{{M}}⌋}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$
162 8 161 eqbrtrd ${⊢}{\phi }\to \left({k}\in {ℤ}_{\ge \left({J}-1\right)}⟼\frac{\left|\parallel \left[\left\{{M}\right\}\right]\cap \left({J}\dots {k}\right)\right|}{{k}}\right)⇝\left(\frac{1}{{M}}\right)$