# 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 )`
` |-  ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> M e. NN )`
` |-  ( ( 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 ) )`
` |-  ( ( ph /\ x e. NN ) -> ( ( NN X. { ( 1 / M ) } ) ` x ) = ( 1 / M ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ph /\ x e. NN ) -> ( 1 / M ) e. RR )`
52 nnre
` |-  ( x e. NN -> x e. RR )`
` |-  ( ( ph /\ x e. NN ) -> x e. RR )`
54 nnne0
` |-  ( x e. NN -> x =/= 0 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ph /\ x e. NN ) -> M e. CC )`
` |-  ( ( 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+ )`
` |-  ( ( ph /\ x e. NN ) -> x e. RR+ )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) )`