Theorem iseraltlem3 13506

Description: Lemma for iseralt 13507. From iseraltlem2 13505, we have (-u1)S(2)(-u1)S() and (-u1)S(1)(-u1)S(21), and we also have (-u1)S(1)= (-u1)S()(1) for each by the definition of the partial sum , so combining the inequalities we get (-u1)S()(1)= (-u1)S(1) (-u1)S(21)= (-u1)S(2)(21) (-u1)S(2)(-u1)S() (-u1)S()(1), so |(-u1)S(21)(-u1)S()|= |S(21)S()|(1) and |(-u1)S(2)(-u1)S()|= |S(2)S()|(1). Thus, both even and odd partial sums are Cauchy if converges to . (Contributed by Mario Carneiro, 6-Apr-2015.)

Hypotheses

Ref	Expression
iseralt.1
iseralt.2
iseralt.3
iseralt.4
iseralt.5
iseralt.6

Assertion

Ref	Expression
iseraltlem3

Distinct variable groups:   ,   ,   ,M   ,   ,   ,N   ,

Proof of Theorem iseraltlem3

Step	Hyp	Ref	Expression
1		neg1rr 10665	. . . . . . . . . 10
2	1	a1i 11	. . . . . . . . 9
3		neg1ne0 10666	. . . . . . . . . 10
4	3	a1i 11	. . . . . . . . 9
5		iseralt.1	. . . . . . . . . . 11
6		uzssz 11129	. . . . . . . . . . 11
7	5, 6	eqsstri 3533	. . . . . . . . . 10
8		simp2 997	. . . . . . . . . 10
9	7, 8	sseldi 3501	. . . . . . . . 9
10	2, 4, 9	reexpclzd 12335	. . . . . . . 8
11	10	recnd 9643	. . . . . . 7
12		iseralt.2	. . . . . . . . . . 11
13		iseralt.6	. . . . . . . . . . . 12
14	1	a1i 11	. . . . . . . . . . . . . 14
15	3	a1i 11	. . . . . . . . . . . . . 14
16		simpr 461	. . . . . . . . . . . . . . 15
17	7, 16	sseldi 3501	. . . . . . . . . . . . . 14
18	14, 15, 17	reexpclzd 12335	. . . . . . . . . . . . 13
19		iseralt.3	. . . . . . . . . . . . . 14
20	19	ffvelrnda 6031	. . . . . . . . . . . . 13
21	18, 20	remulcld 9645	. . . . . . . . . . . 12
22	13, 21	eqeltrd 2545	. . . . . . . . . . 11
23	5, 12, 22	serfre 12136	. . . . . . . . . 10
24	23	3ad2ant1 1017	. . . . . . . . 9
25	8, 5	syl6eleq 2555	. . . . . . . . . . 11
26		2nn0 10837	. . . . . . . . . . . 12
27		simp3 998	. . . . . . . . . . . 12
28		nn0mulcl 10857	. . . . . . . . . . . 12
29	26, 27, 28	sylancr 663	. . . . . . . . . . 11
30		uzaddcl 11166	. . . . . . . . . . 11
31	25, 29, 30	syl2anc 661	. . . . . . . . . 10
32	31, 5	syl6eleqr 2556	. . . . . . . . 9
33	24, 32	ffvelrnd 6032	. . . . . . . 8
34	33	recnd 9643	. . . . . . 7
35	24, 8	ffvelrnd 6032	. . . . . . . 8
36	35	recnd 9643	. . . . . . 7
37	11, 34, 36	subdid 10037	. . . . . 6
38	37	fveq2d 5875	. . . . 5
39	33, 35	resubcld 10012	. . . . . . 7
40	39	recnd 9643	. . . . . 6
41	11, 40	absmuld 13285	. . . . 5
42	38, 41	eqtr3d 2500	. . . 4
43	2	recnd 9643	. . . . . . 7
44		absexpz 13138	. . . . . . 7
45	43, 4, 9, 44	syl3anc 1228	. . . . . 6
46		ax-1cn 9571	. . . . . . . . . 10
47	46	absnegi 13232	. . . . . . . . 9
48		abs1 13130	. . . . . . . . 9
49	47, 48	eqtri 2486	. . . . . . . 8
50	49	oveq1i 6306	. . . . . . 7
51		1exp 12195	. . . . . . . 8
52	9, 51	syl 16	. . . . . . 7
53	50, 52	syl5eq 2510	. . . . . 6
54	45, 53	eqtrd 2498	. . . . 5
55	54	oveq1d 6311	. . . 4
56	40	abscld 13267	. . . . . 6
57	56	recnd 9643	. . . . 5
58	57	mulid2d 9635	. . . 4
59	42, 55, 58	3eqtrd 2502	. . 3
60	10, 35	remulcld 9645	. . . . . 6
61	19	3ad2ant1 1017	. . . . . . 7
62	5	peano2uzs 11164	. . . . . . . 8
63	62	3ad2ant2 1018	. . . . . . 7
64	61, 63	ffvelrnd 6032	. . . . . 6
65	60, 64	resubcld 10012	. . . . 5
66	5	peano2uzs 11164	. . . . . . . 8
67	32, 66	syl 16	. . . . . . 7
68	24, 67	ffvelrnd 6032	. . . . . 6
69	10, 68	remulcld 9645	. . . . 5
70	10, 33	remulcld 9645	. . . . 5
71		seqp1 12122	. . . . . . . . . . 11
72	25, 71	syl 16	. . . . . . . . . 10
73	13	ralrimiva 2871	. . . . . . . . . . . . 13
74	73	3ad2ant1 1017	. . . . . . . . . . . 12
75		fveq2 5871	. . . . . . . . . . . . . 14
76		oveq2 6304	. . . . . . . . . . . . . . 15
77		fveq2 5871	. . . . . . . . . . . . . . 15
78	76, 77	oveq12d 6314	. . . . . . . . . . . . . 14
79	75, 78	eqeq12d 2479	. . . . . . . . . . . . 13
80	79	rspcv 3206	. . . . . . . . . . . 12
81	63, 74, 80	sylc 60	. . . . . . . . . . 11
82	81	oveq2d 6312	. . . . . . . . . 10
83	43, 4, 9	expp1zd 12319	. . . . . . . . . . . . . 14
84		neg1cn 10664	. . . . . . . . . . . . . . 15
85		mulcom 9599	. . . . . . . . . . . . . . 15
86	11, 84, 85	sylancl 662	. . . . . . . . . . . . . 14
87	11	mulm1d 10033	. . . . . . . . . . . . . 14
88	83, 86, 87	3eqtrd 2502	. . . . . . . . . . . . 13
89	88	oveq1d 6311	. . . . . . . . . . . 12
90	64	recnd 9643	. . . . . . . . . . . . 13
91	11, 90	mulneg1d 10034	. . . . . . . . . . . 12
92	89, 91	eqtrd 2498	. . . . . . . . . . 11
93	92	oveq2d 6312	. . . . . . . . . 10
94	72, 82, 93	3eqtrd 2502	. . . . . . . . 9
95	10, 64	remulcld 9645	. . . . . . . . . . 11
96	95	recnd 9643	. . . . . . . . . 10
97	36, 96	negsubd 9960	. . . . . . . . 9
98	94, 97	eqtrd 2498	. . . . . . . 8
99	98	oveq2d 6312	. . . . . . 7
100	11, 36, 96	subdid 10037	. . . . . . 7
101	9	zcnd 10995	. . . . . . . . . . . . . . 15
102	101	2timesd 10806	. . . . . . . . . . . . . 14
103	102	oveq2d 6312	. . . . . . . . . . . . 13
104		2z 10921	. . . . . . . . . . . . . . 15
105	104	a1i 11	. . . . . . . . . . . . . 14
106		expmulz 12212	. . . . . . . . . . . . . 14
107	43, 4, 105, 9, 106	syl22anc 1229	. . . . . . . . . . . . 13
108	103, 107	eqtr3d 2500	. . . . . . . . . . . 12
109		neg1sqe1 12263	. . . . . . . . . . . . 13
110	109	oveq1i 6306	. . . . . . . . . . . 12
111	108, 110	syl6eq 2514	. . . . . . . . . . 11
112		expaddz 12210	. . . . . . . . . . . 12
113	43, 4, 9, 9, 112	syl22anc 1229	. . . . . . . . . . 11
114	111, 113, 52	3eqtr3d 2506	. . . . . . . . . 10
115	114	oveq1d 6311	. . . . . . . . 9
116	11, 11, 90	mulassd 9640	. . . . . . . . 9
117	90	mulid2d 9635	. . . . . . . . 9
118	115, 116, 117	3eqtr3d 2506	. . . . . . . 8
119	118	oveq2d 6312	. . . . . . 7
120	99, 100, 119	3eqtrd 2502	. . . . . 6
121		iseralt.4	. . . . . . . . . . 11
122		iseralt.5	. . . . . . . . . . 11
123	5, 12, 19, 121, 122, 13	iseraltlem2 13505	. . . . . . . . . 10
124	62, 123	syl3an2 1262	. . . . . . . . 9
125		1cnd 9633	. . . . . . . . . . . 12
126	29	nn0cnd 10879	. . . . . . . . . . . 12
127	101, 125, 126	add32d 9825	. . . . . . . . . . 11
128	127	fveq2d 5875	. . . . . . . . . 10
129	88, 128	oveq12d 6314	. . . . . . . . 9
130	88	oveq1d 6311	. . . . . . . . 9
131	124, 129, 130	3brtr3d 4481	. . . . . . . 8
132	68	recnd 9643	. . . . . . . . 9
133	11, 132	mulneg1d 10034	. . . . . . . 8
134	24, 63	ffvelrnd 6032	. . . . . . . . . 10
135	134	recnd 9643	. . . . . . . . 9
136	11, 135	mulneg1d 10034	. . . . . . . 8
137	131, 133, 136	3brtr3d 4481	. . . . . . 7
138	10, 134	remulcld 9645	. . . . . . . 8
139	138, 69	lenegd 10156	. . . . . . 7
140	137, 139	mpbird 232	. . . . . 6
141	120, 140	eqbrtrrd 4474	. . . . 5
142		seqp1 12122	. . . . . . . . . 10
143	31, 142	syl 16	. . . . . . . . 9
144		fveq2 5871	. . . . . . . . . . . . . 14
145		oveq2 6304	. . . . . . . . . . . . . . 15
146		fveq2 5871	. . . . . . . . . . . . . . 15
147	145, 146	oveq12d 6314	. . . . . . . . . . . . . 14
148	144, 147	eqeq12d 2479	. . . . . . . . . . . . 13
149	148	rspcv 3206	. . . . . . . . . . . 12
150	67, 74, 149	sylc 60	. . . . . . . . . . 11
151	7, 63	sseldi 3501	. . . . . . . . . . . . . . 15
152	29	nn0zd 10992	. . . . . . . . . . . . . . 15
153		expaddz 12210	. . . . . . . . . . . . . . 15
154	43, 4, 151, 152, 153	syl22anc 1229	. . . . . . . . . . . . . 14
155	27	nn0zd 10992	. . . . . . . . . . . . . . . . 17
156		expmulz 12212	. . . . . . . . . . . . . . . . 17
157	43, 4, 105, 155, 156	syl22anc 1229	. . . . . . . . . . . . . . . 16
158	109	oveq1i 6306	. . . . . . . . . . . . . . . . 17
159		1exp 12195	. . . . . . . . . . . . . . . . . 18
160	155, 159	syl 16	. . . . . . . . . . . . . . . . 17
161	158, 160	syl5eq 2510	. . . . . . . . . . . . . . . 16
162	157, 161	eqtrd 2498	. . . . . . . . . . . . . . 15
163	88, 162	oveq12d 6314	. . . . . . . . . . . . . 14
164	154, 163	eqtrd 2498	. . . . . . . . . . . . 13
165	127	oveq2d 6312	. . . . . . . . . . . . 13
166	11	negcld 9941	. . . . . . . . . . . . . 14
167	166	mulid1d 9634	. . . . . . . . . . . . 13
168	164, 165, 167	3eqtr3d 2506	. . . . . . . . . . . 12
169	168	oveq1d 6311	. . . . . . . . . . 11
170	61, 67	ffvelrnd 6032	. . . . . . . . . . . . 13
171	170	recnd 9643	. . . . . . . . . . . 12
172	11, 171	mulneg1d 10034	. . . . . . . . . . 11
173	150, 169, 172	3eqtrd 2502	. . . . . . . . . 10
174	173	oveq2d 6312	. . . . . . . . 9
175	10, 170	remulcld 9645	. . . . . . . . . . 11
176	175	recnd 9643	. . . . . . . . . 10
177	34, 176	negsubd 9960	. . . . . . . . 9
178	143, 174, 177	3eqtrd 2502	. . . . . . . 8
179	178	oveq2d 6312	. . . . . . 7
180	11, 34, 176	subdid 10037	. . . . . . 7
181	114	oveq1d 6311	. . . . . . . . 9
182	11, 11, 171	mulassd 9640	. . . . . . . . 9
183	171	mulid2d 9635	. . . . . . . . 9
184	181, 182, 183	3eqtr3d 2506	. . . . . . . 8
185	184	oveq2d 6312	. . . . . . 7
186	179, 180, 185	3eqtrd 2502	. . . . . 6
187		simp1 996	. . . . . . . 8
188	5, 12, 19, 121, 122	iseraltlem1 13504	. . . . . . . 8
189	187, 67, 188	syl2anc 661	. . . . . . 7
190	70, 170	subge02d 10169	. . . . . . 7
191	189, 190	mpbid 210	. . . . . 6
192	186, 191	eqbrtrd 4472	. . . . 5
193	65, 69, 70, 141, 192	letrd 9760	. . . 4
194	60, 64	readdcld 9644	. . . . 5
195	5, 12, 19, 121, 122, 13	iseraltlem2 13505	. . . . 5
196	5, 12, 19, 121, 122	iseraltlem1 13504	. . . . . . 7
197	187, 63, 196	syl2anc 661	. . . . . 6
198	60, 64	addge01d 10165	. . . . . 6
199	197, 198	mpbid 210	. . . . 5
200	70, 60, 194, 195, 199	letrd 9760	. . . 4
201	70, 60, 64	absdifled 13266	. . . 4
202	193, 200, 201	mpbir2and 922	. . 3
203	59, 202	eqbrtrrd 4474	. 2
204	11, 132, 36	subdid 10037	. . . . . 6
205	204	fveq2d 5875	. . . . 5
206	68, 35	resubcld 10012	. . . . . . 7
207	206	recnd 9643	. . . . . 6
208	11, 207	absmuld 13285	. . . . 5
209	205, 208	eqtr3d 2500	. . . 4
210	54	oveq1d 6311	. . . 4
211	207	abscld 13267	. . . . . 6
212	211	recnd 9643	. . . . 5
213	212	mulid2d 9635	. . . 4
214	209, 210, 213	3eqtrd 2502	. . 3
215	69, 70, 194, 192, 200	letrd 9760	. . . 4
216	69, 60, 64	absdifled 13266	. . . 4
217	141, 215, 216	mpbir2and 922	. . 3
218	214, 217	eqbrtrrd 4474	. 2
219	203, 218	jca 532	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807   class class class wbr 4452  -->wf 5589  `cfv 5593  (class class class)co 6296  cc 9511  cr 9512  0cc0 9513  1c1 9514  caddc 9516  cmul 9518  cle 9650  cmin 9828  -ucneg 9829  2c2 10610  cn0 10820  cz 10889  cuz 11110  seqcseq 12107  cexp 12166  cabs 13067  cli 13307

This theorem is referenced by:  iseralt  13507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-er 7330  df-pm 7442  df-en 7537  df-dom 7538  df-sdom 7539  df-sup 7921  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-fz 11702  df-fl 11929  df-seq 12108  df-exp 12167  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-clim 13311  df-rlim 13312