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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
hashnzfzclim.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
Assertion hashnzfzclim ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝐽 − 1 ) ) ↦ ( ( ♯ ‘ ( ( ∥ “ { 𝑀 } ) ∩ ( 𝐽 ... 𝑘 ) ) ) / 𝑘 ) ) ⇝ ( 1 / 𝑀 ) )

Proof

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