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	$⊢ φ \to M \in ℕ$
	hashnzfzclim.j	$⊢ φ \to J \in ℤ$
Assertion	hashnzfzclim	$⊢ φ \to (k \in ℤ_{\geq (J - 1)} ⟼ \frac{\|∥ [\{M\}] \cap (J \dots k)\|}{k}) ⇝ (\frac{1}{M})$

Proof

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

Metamath Proof Explorer

Theorem hashnzfzclim

Proof