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 
|- ( ph -> M e. NN )
hashnzfzclim.j 
|- ( ph -> J e. ZZ )
Assertion hashnzfzclim 
|- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) ) ~~> ( 1 / M ) )

Proof

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