Theorem iseraltlem2 13505

Description: Lemma for iseralt 13507. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S(1)S(3)S(5) and S(4)S(2)S(0) (assuming so that these terms are defined). (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
iseraltlem2

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

Proof of Theorem iseraltlem2

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

Step	Hyp	Ref	Expression
1		oveq2 6304	. . . . . . . . . 10
2		2t0e0 10716	. . . . . . . . . 10
3	1, 2	syl6eq 2514	. . . . . . . . 9
4	3	oveq2d 6312	. . . . . . . 8
5	4	fveq2d 5875	. . . . . . 7
6	5	oveq2d 6312	. . . . . 6
7	6	breq1d 4462	. . . . 5
8	7	imbi2d 316	. . . 4
9		oveq2 6304	. . . . . . . . 9
10	9	oveq2d 6312	. . . . . . . 8
11	10	fveq2d 5875	. . . . . . 7
12	11	oveq2d 6312	. . . . . 6
13	12	breq1d 4462	. . . . 5
14	13	imbi2d 316	. . . 4
15		oveq2 6304	. . . . . . . . 9
16	15	oveq2d 6312	. . . . . . . 8
17	16	fveq2d 5875	. . . . . . 7
18	17	oveq2d 6312	. . . . . 6
19	18	breq1d 4462	. . . . 5
20	19	imbi2d 316	. . . 4
21		oveq2 6304	. . . . . . . . 9
22	21	oveq2d 6312	. . . . . . . 8
23	22	fveq2d 5875	. . . . . . 7
24	23	oveq2d 6312	. . . . . 6
25	24	breq1d 4462	. . . . 5
26	25	imbi2d 316	. . . 4
27		iseralt.1	. . . . . . . . . . . 12
28		uzssz 11129	. . . . . . . . . . . 12
29	27, 28	eqsstri 3533	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	sselda 3503	. . . . . . . . 9
32	31	zcnd 10995	. . . . . . . 8
33	32	addid1d 9801	. . . . . . 7
34	33	fveq2d 5875	. . . . . 6
35	34	oveq2d 6312	. . . . 5
36		neg1rr 10665	. . . . . . . . 9
37		neg1ne0 10666	. . . . . . . . 9
38		reexpclz 12186	. . . . . . . . 9
39	36, 37, 38	mp3an12 1314	. . . . . . . 8
40	31, 39	syl 16	. . . . . . 7
41		iseralt.2	. . . . . . . . 9
42		iseralt.6	. . . . . . . . . 10
43	30	sselda 3503	. . . . . . . . . . . 12
44		reexpclz 12186	. . . . . . . . . . . . 13
45	36, 37, 44	mp3an12 1314	. . . . . . . . . . . 12
46	43, 45	syl 16	. . . . . . . . . . 11
47		iseralt.3	. . . . . . . . . . . 12
48	47	ffvelrnda 6031	. . . . . . . . . . 11
49	46, 48	remulcld 9645	. . . . . . . . . 10
50	42, 49	eqeltrd 2545	. . . . . . . . 9
51	27, 41, 50	serfre 12136	. . . . . . . 8
52	51	ffvelrnda 6031	. . . . . . 7
53	40, 52	remulcld 9645	. . . . . 6
54	53	leidd 10144	. . . . 5
55	35, 54	eqbrtrd 4472	. . . 4
56	47	ad2antrr 725	. . . . . . . . . . 11
57		ax-1cn 9571	. . . . . . . . . . . . . . . 16
58	57	2timesi 10681	. . . . . . . . . . . . . . 15
59	58	oveq2i 6307	. . . . . . . . . . . . . 14
60		simpr 461	. . . . . . . . . . . . . . . . . . 19
61	60, 27	syl6eleq 2555	. . . . . . . . . . . . . . . . . 18
62	61	adantr 465	. . . . . . . . . . . . . . . . 17
63		eluzelz 11119	. . . . . . . . . . . . . . . . 17
64	62, 63	syl 16	. . . . . . . . . . . . . . . 16
65	64	zcnd 10995	. . . . . . . . . . . . . . 15
66		2cn 10631	. . . . . . . . . . . . . . . 16
67		nn0cn 10830	. . . . . . . . . . . . . . . . 17
68	67	adantl 466	. . . . . . . . . . . . . . . 16
69		mulcl 9597	. . . . . . . . . . . . . . . 16
70	66, 68, 69	sylancr 663	. . . . . . . . . . . . . . 15
71	66, 57	mulcli 9622	. . . . . . . . . . . . . . . 16
72	71	a1i 11	. . . . . . . . . . . . . . 15
73	65, 70, 72	addassd 9639	. . . . . . . . . . . . . 14
74	59, 73	syl5eqr 2512	. . . . . . . . . . . . 13
75		2nn0 10837	. . . . . . . . . . . . . . . . . 18
76		simpr 461	. . . . . . . . . . . . . . . . . 18
77		nn0mulcl 10857	. . . . . . . . . . . . . . . . . 18
78	75, 76, 77	sylancr 663	. . . . . . . . . . . . . . . . 17
79		uzaddcl 11166	. . . . . . . . . . . . . . . . 17
80	62, 78, 79	syl2anc 661	. . . . . . . . . . . . . . . 16
81	28, 80	sseldi 3501	. . . . . . . . . . . . . . 15
82	81	zcnd 10995	. . . . . . . . . . . . . 14
83		1cnd 9633	. . . . . . . . . . . . . 14
84	82, 83, 83	addassd 9639	. . . . . . . . . . . . 13
85		2cnd 10633	. . . . . . . . . . . . . . 15
86	85, 68, 83	adddid 9641	. . . . . . . . . . . . . 14
87	86	oveq2d 6312	. . . . . . . . . . . . 13
88	74, 84, 87	3eqtr4d 2508	. . . . . . . . . . . 12
89		peano2nn0 10861	. . . . . . . . . . . . . . . 16
90	89	adantl 466	. . . . . . . . . . . . . . 15
91		nn0mulcl 10857	. . . . . . . . . . . . . . 15
92	75, 90, 91	sylancr 663	. . . . . . . . . . . . . 14
93		uzaddcl 11166	. . . . . . . . . . . . . 14
94	62, 92, 93	syl2anc 661	. . . . . . . . . . . . 13
95	94, 27	syl6eleqr 2556	. . . . . . . . . . . 12
96	88, 95	eqeltrd 2545	. . . . . . . . . . 11
97	56, 96	ffvelrnd 6032	. . . . . . . . . 10
98		peano2uz 11163	. . . . . . . . . . . . 13
99	80, 98	syl 16	. . . . . . . . . . . 12
100	99, 27	syl6eleqr 2556	. . . . . . . . . . 11
101	56, 100	ffvelrnd 6032	. . . . . . . . . 10
102	97, 101	resubcld 10012	. . . . . . . . 9
103		0red 9618	. . . . . . . . 9
104	40	adantr 465	. . . . . . . . . 10
105	51	ad2antrr 725	. . . . . . . . . . 11
106	80, 27	syl6eleqr 2556	. . . . . . . . . . 11
107	105, 106	ffvelrnd 6032	. . . . . . . . . 10
108	104, 107	remulcld 9645	. . . . . . . . 9
109		iseralt.4	. . . . . . . . . . . . 13
110	109	ralrimiva 2871	. . . . . . . . . . . 12
111	110	ad2antrr 725	. . . . . . . . . . 11
112		oveq1 6303	. . . . . . . . . . . . . 14
113	112	fveq2d 5875	. . . . . . . . . . . . 13
114		fveq2 5871	. . . . . . . . . . . . 13
115	113, 114	breq12d 4465	. . . . . . . . . . . 12
116	115	rspcv 3206	. . . . . . . . . . 11
117	100, 111, 116	sylc 60	. . . . . . . . . 10
118	97, 101	suble0d 10168	. . . . . . . . . 10
119	117, 118	mpbird 232	. . . . . . . . 9
120	102, 103, 108, 119	leadd2dd 10192	. . . . . . . 8
121		seqp1 12122	. . . . . . . . . . . . 13
122	99, 121	syl 16	. . . . . . . . . . . 12
123		seqp1 12122	. . . . . . . . . . . . . 14
124	80, 123	syl 16	. . . . . . . . . . . . 13
125	124	oveq1d 6311	. . . . . . . . . . . 12
126	122, 125	eqtrd 2498	. . . . . . . . . . 11
127	88	fveq2d 5875	. . . . . . . . . . 11
128	107	recnd 9643	. . . . . . . . . . . 12
129	42	ralrimiva 2871	. . . . . . . . . . . . . . . . 17
130	129	ad2antrr 725	. . . . . . . . . . . . . . . 16
131		fveq2 5871	. . . . . . . . . . . . . . . . . 18
132		oveq2 6304	. . . . . . . . . . . . . . . . . . 19
133	132, 114	oveq12d 6314	. . . . . . . . . . . . . . . . . 18
134	131, 133	eqeq12d 2479	. . . . . . . . . . . . . . . . 17
135	134	rspcv 3206	. . . . . . . . . . . . . . . 16
136	100, 130, 135	sylc 60	. . . . . . . . . . . . . . 15
137		neg1cn 10664	. . . . . . . . . . . . . . . . . . 19
138	137	a1i 11	. . . . . . . . . . . . . . . . . 18
139	37	a1i 11	. . . . . . . . . . . . . . . . . 18
140	138, 139, 81	expp1zd 12319	. . . . . . . . . . . . . . . . 17
141	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20
142	141, 139, 81	reexpclzd 12335	. . . . . . . . . . . . . . . . . . 19
143	142	recnd 9643	. . . . . . . . . . . . . . . . . 18
144		mulcom 9599	. . . . . . . . . . . . . . . . . 18
145	143, 137, 144	sylancl 662	. . . . . . . . . . . . . . . . 17
146	143	mulm1d 10033	. . . . . . . . . . . . . . . . 17
147	140, 145, 146	3eqtrd 2502	. . . . . . . . . . . . . . . 16
148	147	oveq1d 6311	. . . . . . . . . . . . . . 15
149	101	recnd 9643	. . . . . . . . . . . . . . . 16
150		mulneg12 10020	. . . . . . . . . . . . . . . 16
151	143, 149, 150	syl2anc 661	. . . . . . . . . . . . . . 15
152	136, 148, 151	3eqtrd 2502	. . . . . . . . . . . . . 14
153	101	renegcld 10011	. . . . . . . . . . . . . . 15
154	142, 153	remulcld 9645	. . . . . . . . . . . . . 14
155	152, 154	eqeltrd 2545	. . . . . . . . . . . . 13
156	155	recnd 9643	. . . . . . . . . . . 12
157		fveq2 5871	. . . . . . . . . . . . . . . . . 18
158		oveq2 6304	. . . . . . . . . . . . . . . . . . 19
159		fveq2 5871	. . . . . . . . . . . . . . . . . . 19
160	158, 159	oveq12d 6314	. . . . . . . . . . . . . . . . . 18
161	157, 160	eqeq12d 2479	. . . . . . . . . . . . . . . . 17
162	161	rspcv 3206	. . . . . . . . . . . . . . . 16
163	96, 130, 162	sylc 60	. . . . . . . . . . . . . . 15
164	81	peano2zd 10997	. . . . . . . . . . . . . . . . . 18
165	138, 139, 164	expp1zd 12319	. . . . . . . . . . . . . . . . 17
166	147	oveq1d 6311	. . . . . . . . . . . . . . . . 17
167		mul2neg 10021	. . . . . . . . . . . . . . . . . . 19
168	143, 57, 167	sylancl 662	. . . . . . . . . . . . . . . . . 18
169	143	mulid1d 9634	. . . . . . . . . . . . . . . . . 18
170	168, 169	eqtrd 2498	. . . . . . . . . . . . . . . . 17
171	165, 166, 170	3eqtrd 2502	. . . . . . . . . . . . . . . 16
172	171	oveq1d 6311	. . . . . . . . . . . . . . 15
173	163, 172	eqtrd 2498	. . . . . . . . . . . . . 14
174	142, 97	remulcld 9645	. . . . . . . . . . . . . 14
175	173, 174	eqeltrd 2545	. . . . . . . . . . . . 13
176	175	recnd 9643	. . . . . . . . . . . 12
177	128, 156, 176	addassd 9639	. . . . . . . . . . 11
178	126, 127, 177	3eqtr3d 2506	. . . . . . . . . 10
179	178	oveq2d 6312	. . . . . . . . 9
180	104	recnd 9643	. . . . . . . . . 10
181	155, 175	readdcld 9644	. . . . . . . . . . 11
182	181	recnd 9643	. . . . . . . . . 10
183	180, 128, 182	adddid 9641	. . . . . . . . 9
184	180, 156, 176	adddid 9641	. . . . . . . . . . 11
185	152	oveq2d 6312	. . . . . . . . . . . . . 14
186	153	recnd 9643	. . . . . . . . . . . . . . 15
187	180, 143, 186	mulassd 9640	. . . . . . . . . . . . . 14
188	185, 187	eqtr4d 2501	. . . . . . . . . . . . 13
189	85, 65, 68	adddid 9641	. . . . . . . . . . . . . . . . 17
190	65	2timesd 10806	. . . . . . . . . . . . . . . . . 18
191	190	oveq1d 6311	. . . . . . . . . . . . . . . . 17
192	65, 65, 70	addassd 9639	. . . . . . . . . . . . . . . . 17
193	189, 191, 192	3eqtrrd 2503	. . . . . . . . . . . . . . . 16
194	193	oveq2d 6312	. . . . . . . . . . . . . . 15
195		expaddz 12210	. . . . . . . . . . . . . . . 16
196	138, 139, 64, 81, 195	syl22anc 1229	. . . . . . . . . . . . . . 15
197		2z 10921	. . . . . . . . . . . . . . . . . 18
198	197	a1i 11	. . . . . . . . . . . . . . . . 17
199		nn0z 10912	. . . . . . . . . . . . . . . . . 18
200		zaddcl 10929	. . . . . . . . . . . . . . . . . 18
201	31, 199, 200	syl2an 477	. . . . . . . . . . . . . . . . 17
202		expmulz 12212	. . . . . . . . . . . . . . . . 17
203	138, 139, 198, 201, 202	syl22anc 1229	. . . . . . . . . . . . . . . 16
204		neg1sqe1 12263	. . . . . . . . . . . . . . . . . 18
205	204	oveq1i 6306	. . . . . . . . . . . . . . . . 17
206		1exp 12195	. . . . . . . . . . . . . . . . . 18
207	201, 206	syl 16	. . . . . . . . . . . . . . . . 17
208	205, 207	syl5eq 2510	. . . . . . . . . . . . . . . 16
209	203, 208	eqtrd 2498	. . . . . . . . . . . . . . 15
210	194, 196, 209	3eqtr3d 2506	. . . . . . . . . . . . . 14
211	210	oveq1d 6311	. . . . . . . . . . . . 13
212	186	mulid2d 9635	. . . . . . . . . . . . 13
213	188, 211, 212	3eqtrd 2502	. . . . . . . . . . . 12
214	173	oveq2d 6312	. . . . . . . . . . . . . 14
215	97	recnd 9643	. . . . . . . . . . . . . . 15
216	180, 143, 215	mulassd 9640	. . . . . . . . . . . . . 14
217	214, 216	eqtr4d 2501	. . . . . . . . . . . . 13
218	210	oveq1d 6311	. . . . . . . . . . . . 13
219	215	mulid2d 9635	. . . . . . . . . . . . 13
220	217, 218, 219	3eqtrd 2502	. . . . . . . . . . . 12
221	213, 220	oveq12d 6314	. . . . . . . . . . 11
222	149	negcld 9941	. . . . . . . . . . . . 13
223	222, 215	addcomd 9803	. . . . . . . . . . . 12
224	215, 149	negsubd 9960	. . . . . . . . . . . 12
225	223, 224	eqtrd 2498	. . . . . . . . . . 11
226	184, 221, 225	3eqtrd 2502	. . . . . . . . . 10
227	226	oveq2d 6312	. . . . . . . . 9
228	179, 183, 227	3eqtrrd 2503	. . . . . . . 8
229	108	recnd 9643	. . . . . . . . 9
230	229	addid1d 9801	. . . . . . . 8
231	120, 228, 230	3brtr3d 4481	. . . . . . 7
232	105, 95	ffvelrnd 6032	. . . . . . . . 9
233	104, 232	remulcld 9645	. . . . . . . 8
234	53	adantr 465	. . . . . . . 8
235		letr 9699	. . . . . . . 8
236	233, 108, 234, 235	syl3anc 1228	. . . . . . 7
237	231, 236	mpand 675	. . . . . 6
238	237	expcom 435	. . . . 5
239	238	a2d 26	. . . 4
240	8, 14, 20, 26, 55, 239	nn0ind 10984	. . 3
241	240	com12 31	. 2
242	241	3impia 1193	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  C_wss 3475   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  cli 13307

This theorem is referenced by:  iseraltlem3  13506

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-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

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-en 7537  df-dom 7538  df-sdom 7539  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-n0 10821  df-z 10890  df-uz 11111  df-fz 11702  df-seq 12108  df-exp 12167