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 φ M
hashnzfzclim.j φ J
Assertion hashnzfzclim φ k J 1 M J k k 1 M

Proof

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