Theorem hashnzfzclim 31395

Description: As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 31393 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.)

Hypotheses

Ref	Expression
hashnzfzclim.m	|- ( ph -> M e. NN )
hashnzfzclim.j	|- ( ph -> J e. ZZ )

Assertion

Ref	Expression
hashnzfzclim	|- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) ) ~~> ( 1 / M ) )

Distinct variable groups:   k, J   k, M   ph, k

Proof of Theorem hashnzfzclim

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashnzfzclim.m	. . . . . 6 |- ( ph -> M e. NN )
2	1	adantr 463	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> M e. NN )
3		hashnzfzclim.j	. . . . . 6 |- ( ph -> J e. ZZ )
4	3	adantr 463	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> J e. ZZ )
5		simpr 459	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> k e. ( ZZ>= ` ( J - 1 ) ) )
6	2, 4, 5	hashnzfz 31393	. . . 4 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) = ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) )
7	6	oveq1d 6211	. . 3 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) = ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) )
8	7	mpteq2dva 4453	. 2 |- ( 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 11036	. . . . 5 |- NN = ( ZZ>= ` 1 )
10		1z 10811	. . . . . 6 |- 1 e. ZZ
11	10	a1i 11	. . . . 5 |- ( ph -> 1 e. ZZ )
12	1	nncnd 10468	. . . . . . . . . 10 |- ( ph -> M e. CC )
13	1	nnne0d 10497	. . . . . . . . . 10 |- ( ph -> M =/= 0 )
14	12, 13	reccld 10230	. . . . . . . . 9 |- ( ph -> ( 1 / M ) e. CC )
15	9	eqimss2i 3472	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
16		nnex 10458	. . . . . . . . . 10 |- NN e. _V
17	15, 16	climconst2 13373	. . . . . . . . 9 |- ( ( ( 1 / M ) e. CC /\ 1 e. ZZ ) -> ( NN X. { ( 1 / M ) } ) ~~> ( 1 / M ) )
18	14, 10, 17	sylancl 660	. . . . . . . 8 |- ( ph -> ( NN X. { ( 1 / M ) } ) ~~> ( 1 / M ) )
19	16	mptex 6044	. . . . . . . . 9 |- ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) e. _V
20	19	a1i 11	. . . . . . . 8 |- ( ph -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) e. _V )
21		ax-1cn 9461	. . . . . . . . 9 |- 1 e. CC
22		divcnv 13667	. . . . . . . . 9 |- ( 1 e. CC -> ( k e. NN |-> ( 1 / k ) ) ~~> 0 )
23	21, 22	mp1i 12	. . . . . . . 8 |- ( ph -> ( k e. NN |-> ( 1 / k ) ) ~~> 0 )
24		ovex 6224	. . . . . . . . . . 11 |- ( 1 / M ) e. _V
25	24	fvconst2 6029	. . . . . . . . . 10 |- ( x e. NN -> ( ( NN X. { ( 1 / M ) } ) ` x ) = ( 1 / M ) )
26	25	adantl 464	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( NN X. { ( 1 / M ) } ) ` x ) = ( 1 / M ) )
27	14	adantr 463	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( 1 / M ) e. CC )
28	26, 27	eqeltrd 2470	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( NN X. { ( 1 / M ) } ) ` x ) e. CC )
29		eqidd 2383	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( 1 / k ) ) = ( k e. NN |-> ( 1 / k ) ) )
30		oveq2 6204	. . . . . . . . . . . 12 |- ( k = x -> ( 1 / k ) = ( 1 / x ) )
31	30	adantl 464	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( 1 / k ) = ( 1 / x ) )
32		simpr 459	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> x e. NN )
33		ovex 6224	. . . . . . . . . . . 12 |- ( 1 / x ) e. _V
34	33	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. _V )
35	29, 31, 32, 34	fvmptd 5862	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) = ( 1 / x ) )
36	32	nnrecred 10498	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. RR )
37	35, 36	eqeltrd 2470	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) e. RR )
38	37	recnd 9533	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) e. CC )
39		eqidd 2383	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) = ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) )
40	30	oveq2d 6212	. . . . . . . . . . 11 |- ( k = x -> ( ( 1 / M ) - ( 1 / k ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
41	40	adantl 464	. . . . . . . . . 10 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( 1 / M ) - ( 1 / k ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
42		ovex 6224	. . . . . . . . . . 11 |- ( ( 1 / M ) - ( 1 / x ) ) e. _V
43	42	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) e. _V )
44	39, 41, 32, 43	fvmptd 5862	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) = ( ( 1 / M ) - ( 1 / x ) ) )
45	26, 35	oveq12d 6214	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( NN X. { ( 1 / M ) } ) ` x ) - ( ( k e. NN |-> ( 1 / k ) ) ` x ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
46	44, 45	eqtr4d 2426	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) = ( ( ( NN X. { ( 1 / M ) } ) ` x ) - ( ( k e. NN |-> ( 1 / k ) ) ` x ) ) )
47	9, 11, 18, 20, 23, 28, 38, 46	climsub 13458	. . . . . . 7 |- ( ph -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ~~> ( ( 1 / M ) - 0 ) )
48	14	subid1d 9833	. . . . . . 7 |- ( ph -> ( ( 1 / M ) - 0 ) = ( 1 / M ) )
49	47, 48	breqtrd 4391	. . . . . 6 |- ( ph -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ~~> ( 1 / M ) )
50	16	mptex 6044	. . . . . . 7 |- ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) e. _V
51	50	a1i 11	. . . . . 6 |- ( ph -> ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) e. _V )
52	1	nnrecred 10498	. . . . . . . . 9 |- ( ph -> ( 1 / M ) e. RR )
53	52	adantr 463	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( 1 / M ) e. RR )
54		nnre 10459	. . . . . . . . . 10 |- ( x e. NN -> x e. RR )
55	54	adantl 464	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> x e. RR )
56		nnne0 10485	. . . . . . . . . 10 |- ( x e. NN -> x =/= 0 )
57	56	adantl 464	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> x =/= 0 )
58	55, 57	rereccld 10288	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. RR )
59	53, 58	resubcld 9905	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) e. RR )
60	44, 59	eqeltrd 2470	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) e. RR )
61		eqidd 2383	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) = ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) )
62		oveq1 6203	. . . . . . . . . . 11 |- ( k = x -> ( k / M ) = ( x / M ) )
63	62	fveq2d 5778	. . . . . . . . . 10 |- ( k = x -> ( |_ ` ( k / M ) ) = ( |_ ` ( x / M ) ) )
64		id 22	. . . . . . . . . 10 |- ( k = x -> k = x )
65	63, 64	oveq12d 6214	. . . . . . . . 9 |- ( k = x -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
66	65	adantl 464	. . . . . . . 8 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
67		ovex 6224	. . . . . . . . 9 |- ( ( |_ ` ( x / M ) ) / x ) e. _V
68	67	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) e. _V )
69	61, 66, 32, 68	fvmptd 5862	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) = ( ( |_ ` ( x / M ) ) / x ) )
70	1	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> M e. NN )
71	55, 70	nndivred 10501	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( x / M ) e. RR )
72		reflcl 11832	. . . . . . . . 9 |- ( ( x / M ) e. RR -> ( |_ ` ( x / M ) ) e. RR )
73	71, 72	syl 16	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) e. RR )
74	73, 55, 57	redivcld 10289	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) e. RR )
75	69, 74	eqeltrd 2470	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) e. RR )
76	71	recnd 9533	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( x / M ) e. CC )
77		1cnd 9523	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> 1 e. CC )
78		nncn 10460	. . . . . . . . . . . 12 |- ( x e. NN -> x e. CC )
79	78	adantl 464	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> x e. CC )
80	76, 77, 79, 57	divsubdird 10276	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) = ( ( ( x / M ) / x ) - ( 1 / x ) ) )
81	12	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. NN ) -> M e. CC )
82	13	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. NN ) -> M =/= 0 )
83	79, 81, 82	divrecd 10240	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( x / M ) = ( x x. ( 1 / M ) ) )
84	83	oveq1d 6211	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) / x ) = ( ( x x. ( 1 / M ) ) / x ) )
85	27, 79, 57	divcan3d 10242	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( x x. ( 1 / M ) ) / x ) = ( 1 / M ) )
86	84, 85	eqtrd 2423	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) / x ) = ( 1 / M ) )
87	86	oveq1d 6211	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) / x ) - ( 1 / x ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
88	80, 87	eqtrd 2423	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) = ( ( 1 / M ) - ( 1 / x ) ) )
89		1red 9522	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> 1 e. RR )
90	71, 89	resubcld 9905	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) e. RR )
91		nnrp 11148	. . . . . . . . . . 11 |- ( x e. NN -> x e. RR+ )
92	91	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> x e. RR+ )
93	73, 89	readdcld 9534	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) + 1 ) e. RR )
94		flle 11835	. . . . . . . . . . . . . 14 |- ( ( x / M ) e. RR -> ( |_ ` ( x / M ) ) <_ ( x / M ) )
95	71, 94	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) <_ ( x / M ) )
96		flflp1 11843	. . . . . . . . . . . . . 14 |- ( ( ( x / M ) e. RR /\ ( x / M ) e. RR ) -> ( ( |_ ` ( x / M ) ) <_ ( x / M ) <-> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) ) )
97	71, 71, 96	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) <_ ( x / M ) <-> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) ) )
98	95, 97	mpbid 210	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) )
99	71, 93, 89, 98	ltsub1dd 10081	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) < ( ( ( |_ ` ( x / M ) ) + 1 ) - 1 ) )
100	73	recnd 9533	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) e. CC )
101	100, 77	pncand 9845	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( ( |_ ` ( x / M ) ) + 1 ) - 1 ) = ( |_ ` ( x / M ) ) )
102	99, 101	breqtrd 4391	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) < ( |_ ` ( x / M ) ) )
103	90, 73, 92, 102	ltdiv1dd 11230	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) < ( ( |_ ` ( x / M ) ) / x ) )
104	88, 103	eqbrtrrd 4389	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) < ( ( |_ ` ( x / M ) ) / x ) )
105	59, 74, 104	ltled 9644	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) <_ ( ( |_ ` ( x / M ) ) / x ) )
106		simpr 459	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> k = x )
107	106	oveq1d 6211	. . . . . . . . . 10 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( k / M ) = ( x / M ) )
108	107	fveq2d 5778	. . . . . . . . 9 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( |_ ` ( k / M ) ) = ( |_ ` ( x / M ) ) )
109	108, 106	oveq12d 6214	. . . . . . . 8 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
110	61, 109, 32, 68	fvmptd 5862	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) = ( ( |_ ` ( x / M ) ) / x ) )
111	105, 44, 110	3brtr4d 4397	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) <_ ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) )
112	73, 71, 92, 95	lediv1dd 11231	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) <_ ( ( x / M ) / x ) )
113	112, 86	breqtrd 4391	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) <_ ( 1 / M ) )
114	110, 113	eqbrtrd 4387	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) <_ ( 1 / M ) )
115	9, 11, 49, 51, 60, 75, 111, 114	climsqz 13465	. . . . 5 |- ( ph -> ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ~~> ( 1 / M ) )
116	16	mptex 6044	. . . . . 6 |- ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) e. _V
117	116	a1i 11	. . . . 5 |- ( ph -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) e. _V )
118	3	zred 10884	. . . . . . . . . 10 |- ( ph -> J e. RR )
119		1red 9522	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
120	118, 119	resubcld 9905	. . . . . . . . 9 |- ( ph -> ( J - 1 ) e. RR )
121	120, 1	nndivred 10501	. . . . . . . 8 |- ( ph -> ( ( J - 1 ) / M ) e. RR )
122	121	flcld 11834	. . . . . . 7 |- ( ph -> ( |_ ` ( ( J - 1 ) / M ) ) e. ZZ )
123	122	zcnd 10885	. . . . . 6 |- ( ph -> ( |_ ` ( ( J - 1 ) / M ) ) e. CC )
124		divcnv 13667	. . . . . 6 |- ( ( |_ ` ( ( J - 1 ) / M ) ) e. CC -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ~~> 0 )
125	123, 124	syl 16	. . . . 5 |- ( ph -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ~~> 0 )
126	75	recnd 9533	. . . . 5 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) e. CC )
127		eqidd 2383	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) = ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) )
128		oveq2 6204	. . . . . . . 8 |- ( k = x -> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
129	128	adantl 464	. . . . . . 7 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
130		ovex 6224	. . . . . . . 8 |- ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) e. _V
131	130	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) e. _V )
132	127, 129, 32, 131	fvmptd 5862	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ` x ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
133	123	adantr 463	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( ( J - 1 ) / M ) ) e. CC )
134	133, 79, 57	divcld 10237	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) e. CC )
135	132, 134	eqeltrd 2470	. . . . 5 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ` x ) e. CC )
136	100, 133, 79, 57	divsubdird 10276	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) = ( ( ( |_ ` ( x / M ) ) / x ) - ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) ) )
137		eqidd 2383	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) = ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) )
138	63	oveq1d 6211	. . . . . . . . 9 |- ( k = x -> ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) = ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) )
139	138, 64	oveq12d 6214	. . . . . . . 8 |- ( k = x -> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) = ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) )
140	139	adantl 464	. . . . . . 7 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) = ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) )
141		ovex 6224	. . . . . . . 8 |- ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) e. _V
142	141	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) e. _V )
143	137, 140, 32, 142	fvmptd 5862	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ` x ) = ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) )
144	69, 132	oveq12d 6214	. . . . . 6 |- ( ( 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 ) ) )
145	136, 143, 144	3eqtr4d 2433	. . . . 5 |- ( ( 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 ) ) )
146	9, 11, 115, 117, 125, 126, 135, 145	climsub 13458	. . . 4 |- ( ph -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( ( 1 / M ) - 0 ) )
147	146, 48	breqtrd 4391	. . 3 |- ( ph -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
148		uzssz 11020	. . . . . . 7 |- ( ZZ>= ` ( J - 1 ) ) C_ ZZ
149		resmpt 5235	. . . . . . 7 |- ( ( 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 ) ) )
150	148, 149	ax-mp 5	. . . . . 6 |- ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` ( ZZ>= ` ( J - 1 ) ) ) = ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) )
151	150	breq1i 4374	. . . . 5 |- ( ( ( 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 ) )
152	3, 11	zsubcld 10889	. . . . . 6 |- ( ph -> ( J - 1 ) e. ZZ )
153		zex 10790	. . . . . . 7 |- ZZ e. _V
154	153	mptex 6044	. . . . . 6 |- ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) e. _V
155		climres 13400	. . . . . 6 |- ( ( ( 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 ) ) )
156	152, 154, 155	sylancl 660	. . . . 5 |- ( 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 ) ) )
157	151, 156	syl5bbr 259	. . . 4 |- ( 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 ) ) )
158	9	reseq2i 5183	. . . . . 6 |- ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` NN ) = ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` ( ZZ>= ` 1 ) )
159	158	breq1i 4374	. . . . 5 |- ( ( ( 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 ) )
160		nnssz 10801	. . . . . . 7 |- NN C_ ZZ
161		resmpt 5235	. . . . . . 7 |- ( NN C_ ZZ -> ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` NN ) = ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) )
162	160, 161	ax-mp 5	. . . . . 6 |- ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` NN ) = ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) )
163	162	breq1i 4374	. . . . 5 |- ( ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` NN ) ~~> ( 1 / M ) <-> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
164		climres 13400	. . . . . 6 |- ( ( 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 ) ) )
165	10, 154, 164	mp2an 670	. . . . 5 |- ( ( ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) |` ( ZZ>= ` 1 ) ) ~~> ( 1 / M ) <-> ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
166	159, 163, 165	3bitr3i 275	. . . 4 |- ( ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) <-> ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
167	157, 166	syl6bbr 263	. . 3 |- ( 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 ) ) )
168	147, 167	mpbird 232	. 2 |- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
169	8, 168	eqbrtrd 4387	1 |- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) ) ~~> ( 1 / M ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   e. wcel 1826   =/= wne 2577   _Vcvv 3034   i^i cin 3388   C_ wss 3389   {csn 3944   class class class wbr 4367   |-> cmpt 4425   X. cxp 4911   |` cres 4915   "cima 4916   ` cfv 5496  (class class class)co 6196   CCcc 9401   RRcr 9402   0cc0 9403   1c1 9404   + caddc 9406   x. cmul 9408   < clt 9539   <_ cle 9540   - cmin 9718   / cdiv 10123   NNcn 10452   ZZcz 10781   ZZ>=cuz 11001   RR+crp 11139   ...cfz 11593   |_cfl 11826   #chash 12307   ~~> cli 13309   || cdvds 13988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-pre-sup 9481

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-1o 7048  df-er 7229  df-pm 7341  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-sup 7816  df-card 8233  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-n0 10713  df-z 10782  df-uz 11002  df-rp 11140  df-fz 11594  df-fl 11828  df-seq 12011  df-exp 12070  df-hash 12308  df-cj 12934  df-re 12935  df-im 12936  df-sqrt 13070  df-abs 13071  df-clim 13313  df-rlim 13314  df-dvds 13989

This theorem is referenced by: (None)