Theorem climcndslem2 13662

Description: Lemma for climcnds 13663: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.)

Hypotheses

Ref	Expression
climcnds.1
climcnds.2
climcnds.3
climcnds.4

Assertion

Ref	Expression
climcndslem2

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem climcndslem2

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5871	. . . . 5
2		oveq2 6304	. . . . . . . 8
3		2cn 10631	. . . . . . . . 9
4		exp1 12172	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6	2, 5	syl6eq 2514	. . . . . . 7
7	6	fveq2d 5875	. . . . . 6
8	7	oveq2d 6312	. . . . 5
9	1, 8	breq12d 4465	. . . 4
10	9	imbi2d 316	. . 3
11		fveq2 5871	. . . . 5
12		oveq2 6304	. . . . . . 7
13	12	fveq2d 5875	. . . . . 6
14	13	oveq2d 6312	. . . . 5
15	11, 14	breq12d 4465	. . . 4
16	15	imbi2d 316	. . 3
17		fveq2 5871	. . . . 5
18		oveq2 6304	. . . . . . 7
19	18	fveq2d 5875	. . . . . 6
20	19	oveq2d 6312	. . . . 5
21	17, 20	breq12d 4465	. . . 4
22	21	imbi2d 316	. . 3
23		fveq2 5871	. . . . 5
24		oveq2 6304	. . . . . . 7
25	24	fveq2d 5875	. . . . . 6
26	25	oveq2d 6312	. . . . 5
27	23, 26	breq12d 4465	. . . 4
28	27	imbi2d 316	. . 3
29		1nn 10572	. . . . . . 7
30		climcnds.2	. . . . . . . 8
31	30	ralrimiva 2871	. . . . . . 7
32		fveq2 5871	. . . . . . . . 9
33	32	breq2d 4464	. . . . . . . 8
34	33	rspcv 3206	. . . . . . 7
35	29, 31, 34	mpsyl 63	. . . . . 6
36		2nn 10718	. . . . . . . 8
37		climcnds.1	. . . . . . . . 9
38	37	ralrimiva 2871	. . . . . . . 8
39		fveq2 5871	. . . . . . . . . 10
40	39	eleq1d 2526	. . . . . . . . 9
41	40	rspcv 3206	. . . . . . . 8
42	36, 38, 41	mpsyl 63	. . . . . . 7
43	32	eleq1d 2526	. . . . . . . . 9
44	43	rspcv 3206	. . . . . . . 8
45	29, 38, 44	mpsyl 63	. . . . . . 7
46	42, 45	addge02d 10166	. . . . . 6
47	35, 46	mpbid 210	. . . . 5
48	45, 42	readdcld 9644	. . . . . 6
49		2re 10630	. . . . . . . 8
50		2pos 10652	. . . . . . . 8
51	49, 50	pm3.2i 455	. . . . . . 7
52	51	a1i 11	. . . . . 6
53		lemul2 10420	. . . . . 6
54	42, 48, 52, 53	syl3anc 1228	. . . . 5
55	47, 54	mpbid 210	. . . 4
56		1z 10919	. . . . 5
57		1nn0 10836	. . . . . 6
58		climcnds.4	. . . . . . 7
59	58	ralrimiva 2871	. . . . . 6
60		fveq2 5871	. . . . . . . 8
61		oveq2 6304	. . . . . . . . . 10
62	61, 5	syl6eq 2514	. . . . . . . . 9
63	62	fveq2d 5875	. . . . . . . . 9
64	62, 63	oveq12d 6314	. . . . . . . 8
65	60, 64	eqeq12d 2479	. . . . . . 7
66	65	rspcv 3206	. . . . . 6
67	57, 59, 66	mpsyl 63	. . . . 5
68	56, 67	seq1i 12121	. . . 4
69		nnuz 11145	. . . . . 6
70		df-2 10619	. . . . . 6
71		eqidd 2458	. . . . . . 7
72	56, 71	seq1i 12121	. . . . . 6
73		eqidd 2458	. . . . . 6
74	69, 29, 70, 72, 73	seqp1i 12123	. . . . 5
75	74	oveq2d 6312	. . . 4
76	55, 68, 75	3brtr4d 4482	. . 3
77		peano2nn 10573	. . . . . . . . . . . 12
78	77	adantl 466	. . . . . . . . . . 11
79	78	nnnn0d 10877	. . . . . . . . . 10
80	59	adantr 465	. . . . . . . . . 10
81		fveq2 5871	. . . . . . . . . . . 12
82		oveq2 6304	. . . . . . . . . . . . 13
83	82	fveq2d 5875	. . . . . . . . . . . . 13
84	82, 83	oveq12d 6314	. . . . . . . . . . . 12
85	81, 84	eqeq12d 2479	. . . . . . . . . . 11
86	85	rspcv 3206	. . . . . . . . . 10
87	79, 80, 86	sylc 60	. . . . . . . . 9
88		nnnn0 10827	. . . . . . . . . . . . 13
89	88	adantl 466	. . . . . . . . . . . 12
90		expp1 12173	. . . . . . . . . . . 12
91	3, 89, 90	sylancr 663	. . . . . . . . . . 11
92		nnexpcl 12179	. . . . . . . . . . . . . . 15
93	36, 88, 92	sylancr 663	. . . . . . . . . . . . . 14
94	93	adantl 466	. . . . . . . . . . . . 13
95	94	nncnd 10577	. . . . . . . . . . . 12
96		mulcom 9599	. . . . . . . . . . . 12
97	95, 3, 96	sylancl 662	. . . . . . . . . . 11
98	91, 97	eqtrd 2498	. . . . . . . . . 10
99	98	oveq1d 6311	. . . . . . . . 9
100	3	a1i 11	. . . . . . . . . 10
101		nnexpcl 12179	. . . . . . . . . . . . 13
102	36, 79, 101	sylancr 663	. . . . . . . . . . . 12
103	38	adantr 465	. . . . . . . . . . . 12
104		fveq2 5871	. . . . . . . . . . . . . 14
105	104	eleq1d 2526	. . . . . . . . . . . . 13
106	105	rspcv 3206	. . . . . . . . . . . 12
107	102, 103, 106	sylc 60	. . . . . . . . . . 11
108	107	recnd 9643	. . . . . . . . . 10
109	100, 95, 108	mulassd 9640	. . . . . . . . 9
110	87, 99, 109	3eqtrd 2502	. . . . . . . 8
111	94	nnnn0d 10877	. . . . . . . . . . . . . . 15
112		hashfz1 12419	. . . . . . . . . . . . . . 15
113	111, 112	syl 16	. . . . . . . . . . . . . 14
114	113, 95	eqeltrd 2545	. . . . . . . . . . . . 13
115		fzfid 12083	. . . . . . . . . . . . . . 15
116		hashcl 12428	. . . . . . . . . . . . . . 15
117	115, 116	syl 16	. . . . . . . . . . . . . 14
118	117	nn0cnd 10879	. . . . . . . . . . . . 13
119		simpr 461	. . . . . . . . . . . . . . . . . . 19
120	119	nnzd 10993	. . . . . . . . . . . . . . . . . 18
121		uzid 11124	. . . . . . . . . . . . . . . . . 18
122		peano2uz 11163	. . . . . . . . . . . . . . . . . 18
123		1le2 10774	. . . . . . . . . . . . . . . . . . 19
124		leexp2a 12221	. . . . . . . . . . . . . . . . . . 19
125	49, 123, 124	mp3an12 1314	. . . . . . . . . . . . . . . . . 18
126	120, 121, 122, 125	4syl 21	. . . . . . . . . . . . . . . . 17
127	94, 69	syl6eleq 2555	. . . . . . . . . . . . . . . . . 18
128	102	nnzd 10993	. . . . . . . . . . . . . . . . . 18
129		elfz5 11709	. . . . . . . . . . . . . . . . . 18
130	127, 128, 129	syl2anc 661	. . . . . . . . . . . . . . . . 17
131	126, 130	mpbird 232	. . . . . . . . . . . . . . . 16
132		fzsplit 11740	. . . . . . . . . . . . . . . 16
133	131, 132	syl 16	. . . . . . . . . . . . . . 15
134	133	fveq2d 5875	. . . . . . . . . . . . . 14
135	95	times2d 10807	. . . . . . . . . . . . . . . 16
136	91, 135	eqtrd 2498	. . . . . . . . . . . . . . 15
137	102	nnnn0d 10877	. . . . . . . . . . . . . . . 16
138		hashfz1 12419	. . . . . . . . . . . . . . . 16
139	137, 138	syl 16	. . . . . . . . . . . . . . 15
140	113	oveq1d 6311	. . . . . . . . . . . . . . 15
141	136, 139, 140	3eqtr4d 2508	. . . . . . . . . . . . . 14
142		fzfid 12083	. . . . . . . . . . . . . . 15
143	94	nnred 10576	. . . . . . . . . . . . . . . . 17
144	143	ltp1d 10501	. . . . . . . . . . . . . . . 16
145		fzdisj 11741	. . . . . . . . . . . . . . . 16
146	144, 145	syl 16	. . . . . . . . . . . . . . 15
147		hashun 12450	. . . . . . . . . . . . . . 15
148	142, 115, 146, 147	syl3anc 1228	. . . . . . . . . . . . . 14
149	134, 141, 148	3eqtr3d 2506	. . . . . . . . . . . . 13
150	114, 95, 118, 149	addcanad 9806	. . . . . . . . . . . 12
151	150	oveq1d 6311	. . . . . . . . . . 11
152		fsumconst 13605	. . . . . . . . . . . 12
153	115, 108, 152	syl2anc 661	. . . . . . . . . . 11
154	151, 153	eqtr4d 2501	. . . . . . . . . 10
155	107	adantr 465	. . . . . . . . . . 11
156		simpl 457	. . . . . . . . . . . . 13
157	156	adantr 465	. . . . . . . . . . . 12
158		peano2nn 10573	. . . . . . . . . . . . . 14
159	94, 158	syl 16	. . . . . . . . . . . . 13
160		elfzuz 11713	. . . . . . . . . . . . 13
161		eluznn 11181	. . . . . . . . . . . . 13
162	159, 160, 161	syl2an 477	. . . . . . . . . . . 12
163	157, 162, 37	syl2anc 661	. . . . . . . . . . 11
164		elfzuz3 11714	. . . . . . . . . . . . . . 15
165	164	adantl 466	. . . . . . . . . . . . . 14
166		simplll 759	. . . . . . . . . . . . . . 15
167		elfzuz 11713	. . . . . . . . . . . . . . . . 17
168		eluznn 11181	. . . . . . . . . . . . . . . . 17
169	159, 167, 168	syl2an 477	. . . . . . . . . . . . . . . 16
170		elfzuz 11713	. . . . . . . . . . . . . . . 16
171		eluznn 11181	. . . . . . . . . . . . . . . 16
172	169, 170, 171	syl2an 477	. . . . . . . . . . . . . . 15
173	166, 172, 37	syl2anc 661	. . . . . . . . . . . . . 14
174		simplll 759	. . . . . . . . . . . . . . 15
175		elfzuz 11713	. . . . . . . . . . . . . . . 16
176	169, 175, 171	syl2an 477	. . . . . . . . . . . . . . 15
177		climcnds.3	. . . . . . . . . . . . . . 15
178	174, 176, 177	syl2anc 661	. . . . . . . . . . . . . 14
179	165, 173, 178	monoord2 12138	. . . . . . . . . . . . 13
180	179	ralrimiva 2871	. . . . . . . . . . . 12
181		fveq2 5871	. . . . . . . . . . . . . 14
182	181	breq2d 4464	. . . . . . . . . . . . 13
183	182	rspccva 3209	. . . . . . . . . . . 12
184	180, 183	sylan 471	. . . . . . . . . . 11
185	115, 155, 163, 184	fsumle 13613	. . . . . . . . . 10
186	154, 185	eqbrtrd 4472	. . . . . . . . 9
187	143, 107	remulcld 9645	. . . . . . . . . 10
188	115, 163	fsumrecl 13556	. . . . . . . . . 10
189	51	a1i 11	. . . . . . . . . 10
190		lemul2 10420	. . . . . . . . . 10
191	187, 188, 189, 190	syl3anc 1228	. . . . . . . . 9
192	186, 191	mpbid 210	. . . . . . . 8
193	110, 192	eqbrtrd 4472	. . . . . . 7
194		1zzd 10920	. . . . . . . . . 10
195		nnnn0 10827	. . . . . . . . . . 11
196		simpr 461	. . . . . . . . . . . . . . 15
197		nnexpcl 12179	. . . . . . . . . . . . . . 15
198	36, 196, 197	sylancr 663	. . . . . . . . . . . . . 14
199	198	nnred 10576	. . . . . . . . . . . . 13
200	38	adantr 465	. . . . . . . . . . . . . 14
201		fveq2 5871	. . . . . . . . . . . . . . . 16
202	201	eleq1d 2526	. . . . . . . . . . . . . . 15
203	202	rspcv 3206	. . . . . . . . . . . . . 14
204	198, 200, 203	sylc 60	. . . . . . . . . . . . 13
205	199, 204	remulcld 9645	. . . . . . . . . . . 12
206	58, 205	eqeltrd 2545	. . . . . . . . . . 11
207	195, 206	sylan2 474	. . . . . . . . . 10
208	69, 194, 207	serfre 12136	. . . . . . . . 9
209	208	ffvelrnda 6031	. . . . . . . 8
210	207	ralrimiva 2871	. . . . . . . . . 10
211	210	adantr 465	. . . . . . . . 9
212	81	eleq1d 2526	. . . . . . . . . 10
213	212	rspcv 3206	. . . . . . . . 9
214	78, 211, 213	sylc 60	. . . . . . . 8
215	69, 194, 37	serfre 12136	. . . . . . . . . 10
216		ffvelrn 6029	. . . . . . . . . 10
217	215, 93, 216	syl2an 477	. . . . . . . . 9
218		remulcl 9598	. . . . . . . . 9
219	49, 217, 218	sylancr 663	. . . . . . . 8
220		remulcl 9598	. . . . . . . . 9
221	49, 188, 220	sylancr 663	. . . . . . . 8
222		le2add 10059	. . . . . . . 8
223	209, 214, 219, 221, 222	syl22anc 1229	. . . . . . 7
224	193, 223	mpan2d 674	. . . . . 6
225	119, 69	syl6eleq 2555	. . . . . . . 8
226		seqp1 12122	. . . . . . . 8
227	225, 226	syl 16	. . . . . . 7
228		fzfid 12083	. . . . . . . . . . 11
229		elfznn 11743	. . . . . . . . . . . 12
230	37	recnd 9643	. . . . . . . . . . . 12
231	156, 229, 230	syl2an 477	. . . . . . . . . . 11
232	146, 133, 228, 231	fsumsplit 13562	. . . . . . . . . 10
233		eqidd 2458	. . . . . . . . . . 11
234	102, 69	syl6eleq 2555	. . . . . . . . . . 11
235	233, 234, 231	fsumser 13552	. . . . . . . . . 10
236		eqidd 2458	. . . . . . . . . . . 12
237		elfznn 11743	. . . . . . . . . . . . 13
238	156, 237, 230	syl2an 477	. . . . . . . . . . . 12
239	236, 127, 238	fsumser 13552	. . . . . . . . . . 11
240	239	oveq1d 6311	. . . . . . . . . 10
241	232, 235,