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 syl6bbr
 |-  ( 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 ) )