fsumsplit - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem fsumsplit 8280

Description: Split a finite sum into two parts. Warning: The HTML proof page is 0.6 megabyte in size.

**Assertion**
Ref	Expression
fsumsplit	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem fsumsplit**
Step	Hyp	Ref	Expression
1		breq1 3341	. . . . . . . . 9
2	1	anbi2d 678	. . . . . . . 8 $/\$ $/\$
3	2	anbi1d 679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
4		opreq2 4890	. . . . . . . . . 10
5	4	sumeq1d 8250	. . . . . . . . 9
6		opreq1 4889	. . . . . . . . . . 11
7	6	opreq1d 4897	. . . . . . . . . 10
8	7	sumeq1d 8250	. . . . . . . . 9
9	5, 8	opreq12d 4900	. . . . . . . 8
10	9	eqeq2d 1895	. . . . . . 7
11	3, 10	imbi12d 688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
12		breq1 3341	. . . . . . . . 9
13	12	anbi2d 678	. . . . . . . 8 $/\$ $/\$
14	13	anbi1d 679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		opreq2 4890	. . . . . . . . . 10
16	15	sumeq1d 8250	. . . . . . . . 9
17		opreq1 4889	. . . . . . . . . . 11
18	17	opreq1d 4897	. . . . . . . . . 10
19	18	sumeq1d 8250	. . . . . . . . 9
20	16, 19	opreq12d 4900	. . . . . . . 8
21	20	eqeq2d 1895	. . . . . . 7
22	14, 21	imbi12d 688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
23		breq1 3341	. . . . . . . . 9
24	23	anbi2d 678	. . . . . . . 8 $/\$ $/\$
25	24	anbi1d 679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
26		opreq2 4890	. . . . . . . . . 10
27	26	sumeq1d 8250	. . . . . . . . 9
28		opreq1 4889	. . . . . . . . . . 11
29	28	opreq1d 4897	. . . . . . . . . 10
30	29	sumeq1d 8250	. . . . . . . . 9
31	27, 30	opreq12d 4900	. . . . . . . 8
32	31	eqeq2d 1895	. . . . . . 7
33	25, 32	imbi12d 688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
34		breq1 3341	. . . . . . . . 9
35	34	anbi2d 678	. . . . . . . 8 $/\$ $/\$
36	35	anbi1d 679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
37		opreq2 4890	. . . . . . . . . 10
38	37	sumeq1d 8250	. . . . . . . . 9
39		opreq1 4889	. . . . . . . . . . 11
40	39	opreq1d 4897	. . . . . . . . . 10
41	40	sumeq1d 8250	. . . . . . . . 9
42	38, 41	opreq12d 4900	. . . . . . . 8
43	42	eqeq2d 1895	. . . . . . 7
44	36, 43	imbi12d 688	. . . . . 6 $/\$ $/\$ $/\$ $/\$
45		fsum1ps 8278	. . . . . . . . . . 11 $/\$ $/\$
46	45	3expa 1067	. . . . . . . . . 10 $/\$ $/\$
47		eluzel2 7593	. . . . . . . . . . . . . . . . . 18
48		fzss2 7676	. . . . . . . . . . . . . . . . . 18 $/\$
49	47, 48	mpdan 768	. . . . . . . . . . . . . . . . 17
50	49	sseld 2619	. . . . . . . . . . . . . . . 16
51	50	imim1d 33	. . . . . . . . . . . . . . 15
52	51	ralimdv2 2173	. . . . . . . . . . . . . 14
53	52	imp 377	. . . . . . . . . . . . 13 $/\$
54		fsum1s 8269	. . . . . . . . . . . . . 14 $/\$
55	54, 47	sylan 497	. . . . . . . . . . . . 13 $/\$
56	53, 55	syldan 516	. . . . . . . . . . . 12 $/\$
57	56	adantlr 429	. . . . . . . . . . 11 $/\$ $/\$
58	57	opreq1d 4897	. . . . . . . . . 10 $/\$ $/\$
59	46, 58	eqtr4d 1928	. . . . . . . . 9 $/\$ $/\$
60		ltle 6690	. . . . . . . . . . . 12 $/\$
61		zre 7348	. . . . . . . . . . . 12
62		zre 7348	. . . . . . . . . . . 12
63	60, 61, 62	syl2an 503	. . . . . . . . . . 11 $/\$
64		eluz 7595	. . . . . . . . . . 11 $/\$
65	63, 64	sylibrd 221	. . . . . . . . . 10 $/\$
66	65	impac 423	. . . . . . . . 9 $/\$ $/\$ $/\$
67	59, 66	sylan 497	. . . . . . . 8 $/\$ $/\$ $/\$
68	67	exp41 413	. . . . . . 7
69	68	imp4c 393	. . . . . 6 $/\$ $/\$
70		eluzelz 7592	. . . . . . . . . . 11
71		ltp1 6989	. . . . . . . . . . . . . . 15
72	71	adantr 425	. . . . . . . . . . . . . 14 $/\$
73		axlttrn 6673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
74	73	3expa 1067	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		peano2re 6599	. . . . . . . . . . . . . . . 16
76	75	ancli 320	. . . . . . . . . . . . . . 15 $/\$
77	74, 76	sylan 497	. . . . . . . . . . . . . 14 $/\$ $/\$
78	72, 77	mpand 765	. . . . . . . . . . . . 13 $/\$
79		zre 7348	. . . . . . . . . . . . 13
80	78, 79, 62	syl2an 503	. . . . . . . . . . . 12 $/\$
81	80	ex 402	. . . . . . . . . . 11
82	70, 81	syl 12	. . . . . . . . . 10
83	82	imdistand 493	. . . . . . . . 9 $/\$ $/\$
84	83	anim1d 619	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
85	84	imim1d 33	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
86		id 73	. . . . . . . . . . . 12
87		simplll 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
88		ltle 6690	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
89		zre 7348	. . . . . . . . . . . . . . . . . . . . . . . 24
90	88, 89, 62	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91	90	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
92		eluz 7595	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
94	91, 93	mpbird 213	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
95	70	peano2zdi 7376	. . . . . . . . . . . . . . . . . . . . 21
96	94, 95	sylanl1 509	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
97		eluzel2 7593	. . . . . . . . . . . . . . . . . . . . 21
98	97	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
99		fzss2 7676	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	96, 98, 99	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	100	sseld 2619	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102	101	imim1d 33	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
103	102	ralimdv2 2173	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	103	imp 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
105		fsump1s 8273	. . . . . . . . . . . . . . 15 $/\$
106	87, 104, 105	syl11anc 524	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	90, 92	sylibrd 221	. . . . . . . . . . . . . . . . . . . . 21 $/\$
108	107, 95	sylan 497	. . . . . . . . . . . . . . . . . . . 20 $/\$
109	108	imp 377	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
110	109	adantr 425	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
111		simplr 449	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
112		fzss1 7675	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113		peano2uz 7616	. . . . . . . . . . . . . . . . . . . . . . . 24
114	112, 113	sylan 497	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
115	114	sseld 2619	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	115	imim1d 33	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	116	ralimdv2 2173	. . . . . . . . . . . . . . . . . . . 20 $/\$
118	117	imp 377	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119	118	adantlr 429	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
120		fsum1ps 8278	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
121	110, 111, 119, 120	syl111anc 1100	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
122	121	eqcomd 1889	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
123		fsumcl 8275	. . . . . . . . . . . . . . . . . . 19 $/\$
124	123, 96	sylan 497	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
125	119, 124	syldan 516	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
126		ra4csbela 2587	. . . . . . . . . . . . . . . . . 18 $/\$
127	113	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
128		eluzfz 7647	. . . . . . . . . . . . . . . . . . 19 $/\$
129	127, 96, 128	syl11anc 524	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
130	126, 129	sylan 497	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
131		fzss1 7675	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
132		peano2uz 7616	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	131, 132	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
134	133	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135	134	imim1d 33	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
136	135	ralimdv2 2173	. . . . . . . . . . . . . . . . . . . . 21 $/\$
137	136	imp 377	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
138	137	adantlr 429	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139		fsumcl 8275	. . . . . . . . . . . . . . . . . . . 20 $/\$
140		eluz 7595	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
141		eluzelz 7592	. . . . . . . . . . . . . . . . . . . . . . 23
142	141	peano2zdi 7376	. . . . . . . . . . . . . . . . . . . . . 22
143	140, 142	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 $/\$
144	143	biimpar 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
145	139, 144	sylan 497	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
146	138, 145	syldan 516	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
147		simpl 346	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
148		zltp1le 7390	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
149	148, 141	sylan 497	. . . . . . . . . . . . . . . . . . . . 21 $/\$
150	149	biimpa 460	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
151	147, 150	jca 310	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
152	151, 113	sylanl1 509	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
153	146, 152	sylan 497	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
154		subadd 6532	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
155	125, 130, 153, 154	syl111anc 1100	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
156	122, 155	mpbird 213	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
157	156	eqcomd 1889	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
158	106, 157	opreq12d 4900	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
159		ltle 6690	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	78, 159	syld 30	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
161	160, 79, 62	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
162	161	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
163		eluz 7595	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
164	163	biimpar 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
165	162, 164	syldan 516	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
166	165, 70	sylanl1 509	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
167		fzss2 7676	. . . . . . . . . . . . . . . . . . . 20 $/\$
168	166, 98, 167	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169	168	sseld 2619	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	169	imim1d 33	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
171	170	ralimdv2 2173	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172	171	imp 377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
173		fsumcl 8275	. . . . . . . . . . . . . . . 16 $/\$
174		simpll 448	. . . . . . . . . . . . . . . 16 $/\$ $/\$
175	173, 174	sylan 497	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	172, 175	syldan 516	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177		ppncan 6648	. . . . . . . . . . . . . 14 $/\$ $/\$
178	176, 130, 125, 177	syl111anc 1100	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179	158, 178	eqtr2d 1926	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180	86, 179	sylan9eqr 1951	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
181	180	ex 402	. . . . . . . . . 10 $/\$ $/\$ $/\$
182	181	exp41 413	. . . . . . . . 9
183	182	imp4c 393	. . . . . . . 8 $/\$ $/\$
184	183	a2d 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
185	85, 184	syld 30	. . . . . 6 $/\$ $/\$ $/\$ $/\$
186	11, 22, 33, 44, 69, 185	uzind4 7619	. . . . 5 $/\$ $/\$
187	186	exp3a 405	. . . 4 $/\$
188	187	imp31 389	. . 3 $/\$ $/\$ $/\$
189		elfzuz 7658	. . . . 5
190	189	adantl 424	. . . 4 $/\$
191		simpl 346	. . . 4 $/\$
192		zltlem1 7393	. . . . . . . 8 $/\$
193	192	ancoms 484	. . . . . . 7 $/\$
194	193	biimpar 461	. . . . . 6 $/\$ $/\$
195	194	anasss 488	. . . . 5 $/\$ $/\$
196		elfzelz 7652	. . . . . 6
197		elfzle2 7654	. . . . . 6
198	196, 197	jca 310	. . . . 5 $/\$
199	195, 198	sylan2 500	. . . 4 $/\$
200	190, 191, 199	jca32 312	. . 3 $/\$ $/\$ $/\$
201	188, 200	sylan 497	. 2 $/\$ $/\$
202	201	3impa 1062	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wral 2105

csb 2540

wss 2593 class class class wbr 3338

cfv 3998 (class class class)co 4884

cc 6384

cr 6385

c1 6387

caddc 6389

cmin 6445

cle 6448

cz 6451

clt 6653

cuz 7586

cfz 7637

csu 8239

This theorem is referenced by: fsum0split 8281 fsumcmpndx2 8302 serzsplit 8316 fsumlt1 15831

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-n 7108 df-n0 7309 df-z 7345 df-uz 7587 df-fz 7638 df-seq1 7721 df-shft 7754 df-seqz 7776 df-sum 8240