Theorem hashnzfzclim 36665

Description: As the upper bound K of the constraint interval ( J ... K ) in hashnzfz 36663 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 467	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> M e. NN )
3		hashnzfzclim.j	. . . . . 6 |- ( ph -> J e. ZZ )
4	3	adantr 467	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> J e. ZZ )
5		simpr 463	. . . . 5 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> k e. ( ZZ>= ` ( J - 1 ) ) )
6	2, 4, 5	hashnzfz 36663	. . . 4 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) = ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) )
7	6	oveq1d 6303	. . 3 |- ( ( ph /\ k e. ( ZZ>= ` ( J - 1 ) ) ) -> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) = ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) )
8	7	mpteq2dva 4488	. 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 11191	. . . . 5 |- NN = ( ZZ>= ` 1 )
10		1z 10964	. . . . . 6 |- 1 e. ZZ
11	10	a1i 11	. . . . 5 |- ( ph -> 1 e. ZZ )
12	1	nncnd 10622	. . . . . . . . . 10 |- ( ph -> M e. CC )
13	1	nnne0d 10651	. . . . . . . . . 10 |- ( ph -> M =/= 0 )
14	12, 13	reccld 10373	. . . . . . . . 9 |- ( ph -> ( 1 / M ) e. CC )
15	9	eqimss2i 3486	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
16		nnex 10612	. . . . . . . . . 10 |- NN e. _V
17	15, 16	climconst2 13605	. . . . . . . . 9 |- ( ( ( 1 / M ) e. CC /\ 1 e. ZZ ) -> ( NN X. { ( 1 / M ) } ) ~~> ( 1 / M ) )
18	14, 10, 17	sylancl 667	. . . . . . . 8 |- ( ph -> ( NN X. { ( 1 / M ) } ) ~~> ( 1 / M ) )
19	16	mptex 6134	. . . . . . . . 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 9594	. . . . . . . . 9 |- 1 e. CC
22		divcnv 13904	. . . . . . . . 9 |- ( 1 e. CC -> ( k e. NN |-> ( 1 / k ) ) ~~> 0 )
23	21, 22	mp1i 13	. . . . . . . 8 |- ( ph -> ( k e. NN |-> ( 1 / k ) ) ~~> 0 )
24		ovex 6316	. . . . . . . . . . 11 |- ( 1 / M ) e. _V
25	24	fvconst2 6118	. . . . . . . . . 10 |- ( x e. NN -> ( ( NN X. { ( 1 / M ) } ) ` x ) = ( 1 / M ) )
26	25	adantl 468	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( NN X. { ( 1 / M ) } ) ` x ) = ( 1 / M ) )
27	14	adantr 467	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( 1 / M ) e. CC )
28	26, 27	eqeltrd 2528	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( NN X. { ( 1 / M ) } ) ` x ) e. CC )
29		eqidd 2451	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( 1 / k ) ) = ( k e. NN |-> ( 1 / k ) ) )
30		oveq2 6296	. . . . . . . . . . . 12 |- ( k = x -> ( 1 / k ) = ( 1 / x ) )
31	30	adantl 468	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( 1 / k ) = ( 1 / x ) )
32		simpr 463	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> x e. NN )
33		ovex 6316	. . . . . . . . . . . 12 |- ( 1 / x ) e. _V
34	33	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. _V )
35	29, 31, 32, 34	fvmptd 5952	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) = ( 1 / x ) )
36	32	nnrecred 10652	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. RR )
37	35, 36	eqeltrd 2528	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) e. RR )
38	37	recnd 9666	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( 1 / k ) ) ` x ) e. CC )
39		eqidd 2451	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) = ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) )
40	30	oveq2d 6304	. . . . . . . . . . 11 |- ( k = x -> ( ( 1 / M ) - ( 1 / k ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
41	40	adantl 468	. . . . . . . . . 10 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( 1 / M ) - ( 1 / k ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
42		ovex 6316	. . . . . . . . . . 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 5952	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) = ( ( 1 / M ) - ( 1 / x ) ) )
45	26, 35	oveq12d 6306	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( NN X. { ( 1 / M ) } ) ` x ) - ( ( k e. NN |-> ( 1 / k ) ) ` x ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
46	44, 45	eqtr4d 2487	. . . . . . . 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 13690	. . . . . . 7 |- ( ph -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ~~> ( ( 1 / M ) - 0 ) )
48	14	subid1d 9972	. . . . . . 7 |- ( ph -> ( ( 1 / M ) - 0 ) = ( 1 / M ) )
49	47, 48	breqtrd 4426	. . . . . 6 |- ( ph -> ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ~~> ( 1 / M ) )
50	16	mptex 6134	. . . . . . 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 10652	. . . . . . . . 9 |- ( ph -> ( 1 / M ) e. RR )
53	52	adantr 467	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( 1 / M ) e. RR )
54		nnre 10613	. . . . . . . . . 10 |- ( x e. NN -> x e. RR )
55	54	adantl 468	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> x e. RR )
56		nnne0 10639	. . . . . . . . . 10 |- ( x e. NN -> x =/= 0 )
57	56	adantl 468	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> x =/= 0 )
58	55, 57	rereccld 10431	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( 1 / x ) e. RR )
59	53, 58	resubcld 10044	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) e. RR )
60	44, 59	eqeltrd 2528	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( 1 / M ) - ( 1 / k ) ) ) ` x ) e. RR )
61		eqidd 2451	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) = ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) )
62		oveq1 6295	. . . . . . . . . . 11 |- ( k = x -> ( k / M ) = ( x / M ) )
63	62	fveq2d 5867	. . . . . . . . . 10 |- ( k = x -> ( |_ ` ( k / M ) ) = ( |_ ` ( x / M ) ) )
64		id 22	. . . . . . . . . 10 |- ( k = x -> k = x )
65	63, 64	oveq12d 6306	. . . . . . . . 9 |- ( k = x -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
66	65	adantl 468	. . . . . . . 8 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
67		ovex 6316	. . . . . . . . 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 5952	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) = ( ( |_ ` ( x / M ) ) / x ) )
70	1	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> M e. NN )
71	55, 70	nndivred 10655	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( x / M ) e. RR )
72		reflcl 12029	. . . . . . . . 9 |- ( ( x / M ) e. RR -> ( |_ ` ( x / M ) ) e. RR )
73	71, 72	syl 17	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) e. RR )
74	73, 55, 57	redivcld 10432	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) e. RR )
75	69, 74	eqeltrd 2528	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) e. RR )
76	71	recnd 9666	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( x / M ) e. CC )
77		1cnd 9656	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> 1 e. CC )
78		nncn 10614	. . . . . . . . . . . 12 |- ( x e. NN -> x e. CC )
79	78	adantl 468	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> x e. CC )
80	76, 77, 79, 57	divsubdird 10419	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) = ( ( ( x / M ) / x ) - ( 1 / x ) ) )
81	12	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. NN ) -> M e. CC )
82	13	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. NN ) -> M =/= 0 )
83	79, 81, 82	divrecd 10383	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( x / M ) = ( x x. ( 1 / M ) ) )
84	83	oveq1d 6303	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) / x ) = ( ( x x. ( 1 / M ) ) / x ) )
85	27, 79, 57	divcan3d 10385	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( x x. ( 1 / M ) ) / x ) = ( 1 / M ) )
86	84, 85	eqtrd 2484	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) / x ) = ( 1 / M ) )
87	86	oveq1d 6303	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) / x ) - ( 1 / x ) ) = ( ( 1 / M ) - ( 1 / x ) ) )
88	80, 87	eqtrd 2484	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) = ( ( 1 / M ) - ( 1 / x ) ) )
89		1red 9655	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> 1 e. RR )
90	71, 89	resubcld 10044	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) e. RR )
91		nnrp 11308	. . . . . . . . . . 11 |- ( x e. NN -> x e. RR+ )
92	91	adantl 468	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> x e. RR+ )
93	73, 89	readdcld 9667	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) + 1 ) e. RR )
94		flle 12032	. . . . . . . . . . . . . 14 |- ( ( x / M ) e. RR -> ( |_ ` ( x / M ) ) <_ ( x / M ) )
95	71, 94	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) <_ ( x / M ) )
96		flflp1 12040	. . . . . . . . . . . . . 14 |- ( ( ( x / M ) e. RR /\ ( x / M ) e. RR ) -> ( ( |_ ` ( x / M ) ) <_ ( x / M ) <-> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) ) )
97	71, 71, 96	syl2anc 666	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) <_ ( x / M ) <-> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) ) )
98	95, 97	mpbid 214	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( x / M ) < ( ( |_ ` ( x / M ) ) + 1 ) )
99	71, 93, 89, 98	ltsub1dd 10222	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) < ( ( ( |_ ` ( x / M ) ) + 1 ) - 1 ) )
100	73	recnd 9666	. . . . . . . . . . . 12 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( x / M ) ) e. CC )
101	100, 77	pncand 9984	. . . . . . . . . . 11 |- ( ( ph /\ x e. NN ) -> ( ( ( |_ ` ( x / M ) ) + 1 ) - 1 ) = ( |_ ` ( x / M ) ) )
102	99, 101	breqtrd 4426	. . . . . . . . . 10 |- ( ( ph /\ x e. NN ) -> ( ( x / M ) - 1 ) < ( |_ ` ( x / M ) ) )
103	90, 73, 92, 102	ltdiv1dd 11392	. . . . . . . . 9 |- ( ( ph /\ x e. NN ) -> ( ( ( x / M ) - 1 ) / x ) < ( ( |_ ` ( x / M ) ) / x ) )
104	88, 103	eqbrtrrd 4424	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) < ( ( |_ ` ( x / M ) ) / x ) )
105	59, 74, 104	ltled 9780	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( 1 / M ) - ( 1 / x ) ) <_ ( ( |_ ` ( x / M ) ) / x ) )
106		simpr 463	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> k = x )
107	106	oveq1d 6303	. . . . . . . . . 10 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( k / M ) = ( x / M ) )
108	107	fveq2d 5867	. . . . . . . . 9 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( |_ ` ( k / M ) ) = ( |_ ` ( x / M ) ) )
109	108, 106	oveq12d 6306	. . . . . . . 8 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( k / M ) ) / k ) = ( ( |_ ` ( x / M ) ) / x ) )
110	61, 109, 32, 68	fvmptd 5952	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) = ( ( |_ ` ( x / M ) ) / x ) )
111	105, 44, 110	3brtr4d 4432	. . . . . 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 11393	. . . . . . . 8 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) <_ ( ( x / M ) / x ) )
113	112, 86	breqtrd 4426	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( x / M ) ) / x ) <_ ( 1 / M ) )
114	110, 113	eqbrtrd 4422	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) <_ ( 1 / M ) )
115	9, 11, 49, 51, 60, 75, 111, 114	climsqz 13697	. . . . 5 |- ( ph -> ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ~~> ( 1 / M ) )
116	16	mptex 6134	. . . . . 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 11037	. . . . . . . . . 10 |- ( ph -> J e. RR )
119		1red 9655	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
120	118, 119	resubcld 10044	. . . . . . . . 9 |- ( ph -> ( J - 1 ) e. RR )
121	120, 1	nndivred 10655	. . . . . . . 8 |- ( ph -> ( ( J - 1 ) / M ) e. RR )
122	121	flcld 12031	. . . . . . 7 |- ( ph -> ( |_ ` ( ( J - 1 ) / M ) ) e. ZZ )
123	122	zcnd 11038	. . . . . 6 |- ( ph -> ( |_ ` ( ( J - 1 ) / M ) ) e. CC )
124		divcnv 13904	. . . . . 6 |- ( ( |_ ` ( ( J - 1 ) / M ) ) e. CC -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ~~> 0 )
125	123, 124	syl 17	. . . . 5 |- ( ph -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ~~> 0 )
126	75	recnd 9666	. . . . 5 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( k / M ) ) / k ) ) ` x ) e. CC )
127		eqidd 2451	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) = ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) )
128		oveq2 6296	. . . . . . . 8 |- ( k = x -> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
129	128	adantl 468	. . . . . . 7 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
130		ovex 6316	. . . . . . . 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 5952	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ` x ) = ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) )
133	123	adantr 467	. . . . . . 7 |- ( ( ph /\ x e. NN ) -> ( |_ ` ( ( J - 1 ) / M ) ) e. CC )
134	133, 79, 57	divcld 10380	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) e. CC )
135	132, 134	eqeltrd 2528	. . . . 5 |- ( ( ph /\ x e. NN ) -> ( ( k e. NN |-> ( ( |_ ` ( ( J - 1 ) / M ) ) / k ) ) ` x ) e. CC )
136	100, 133, 79, 57	divsubdird 10419	. . . . . 6 |- ( ( ph /\ x e. NN ) -> ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) = ( ( ( |_ ` ( x / M ) ) / x ) - ( ( |_ ` ( ( J - 1 ) / M ) ) / x ) ) )
137		eqidd 2451	. . . . . . 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 6303	. . . . . . . . 9 |- ( k = x -> ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) = ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) )
139	138, 64	oveq12d 6306	. . . . . . . 8 |- ( k = x -> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) = ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) )
140	139	adantl 468	. . . . . . 7 |- ( ( ( ph /\ x e. NN ) /\ k = x ) -> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) = ( ( ( |_ ` ( x / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / x ) )
141		ovex 6316	. . . . . . . 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 5952	. . . . . 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 6306	. . . . . 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 2494	. . . . 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 13690	. . . 4 |- ( ph -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( ( 1 / M ) - 0 ) )
147	146, 48	breqtrd 4426	. . 3 |- ( ph -> ( k e. NN |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
148		uzssz 11175	. . . . . . 7 |- ( ZZ>= ` ( J - 1 ) ) C_ ZZ
149		resmpt 5153	. . . . . . 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 4408	. . . . 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 11042	. . . . . 6 |- ( ph -> ( J - 1 ) e. ZZ )
153		zex 10943	. . . . . . 7 |- ZZ e. _V
154	153	mptex 6134	. . . . . 6 |- ( k e. ZZ |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) e. _V
155		climres 13632	. . . . . 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 667	. . . . 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 263	. . . 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 5101	. . . . . 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 4408	. . . . 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 10954	. . . . . . 7 |- NN C_ ZZ
161		resmpt 5153	. . . . . . 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 4408	. . . . 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 13632	. . . . . 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 677	. . . . 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 279	. . . 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 267	. . 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 236	. 2 |- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( ( |_ ` ( k / M ) ) - ( |_ ` ( ( J - 1 ) / M ) ) ) / k ) ) ~~> ( 1 / M ) )
169	8, 168	eqbrtrd 4422	1 |- ( ph -> ( k e. ( ZZ>= ` ( J - 1 ) ) |-> ( ( # ` ( ( || " { M } ) i^i ( J ... k ) ) ) / k ) ) ~~> ( 1 / M ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   =/= wne 2621   _Vcvv 3044   i^i cin 3402   C_ wss 3403   {csn 3967   class class class wbr 4401   |-> cmpt 4460   X. cxp 4831   |` cres 4835   "cima 4836   ` cfv 5581  (class class class)co 6288   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537   + caddc 9539   x. cmul 9541   < clt 9672   <_ cle 9673   - cmin 9857   / cdiv 10266   NNcn 10606   ZZcz 10934   ZZ>=cuz 11156   RR+crp 11299   ...cfz 11781   |_cfl 12023   #chash 12512   ~~> cli 13541   || cdvds 14298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-er 7360  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-sup 7953  df-inf 7954  df-card 8370  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-rp 11300  df-fz 11782  df-fl 12025  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-rlim 13546  df-dvds 14299

This theorem is referenced by: (None)