Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem fsumadd 6960

Description: The sum of two finite sums.

Assertion

Ref	Expression
fsumadd

Distinct variable groups:   ,   ,

---

Proof of Theorem fsumadd

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . 5
2	1	raleq1d 1781	. . . 4
3	1	sumeq1d 6928	. . . . 5
4	1	sumeq1d 6928	. . . . . 6
5	1	sumeq1d 6928	. . . . . 6
6	4, 5	opreq12d 3963	. . . . 5
7	3, 6	eqeq12d 1481	. . . 4
8	2, 7	imbi12d 624	. . 3
9		opreq2 3954	. . . . 5
10	9	raleq1d 1781	. . . 4
11	9	sumeq1d 6928	. . . . 5
12	9	sumeq1d 6928	. . . . . 6
13	9	sumeq1d 6928	. . . . . 6
14	12, 13	opreq12d 3963	. . . . 5
15	11, 14	eqeq12d 1481	. . . 4
16	10, 15	imbi12d 624	. . 3
17		opreq2 3954	. . . . 5
18	17	raleq1d 1781	. . . 4
19	17	sumeq1d 6928	. . . . 5
20	17	sumeq1d 6928	. . . . . 6
21	17	sumeq1d 6928	. . . . . 6
22	20, 21	opreq12d 3963	. . . . 5
23	19, 22	eqeq12d 1481	. . . 4
24	18, 23	imbi12d 624	. . 3
25		opreq2 3954	. . . . 5
26	25	raleq1d 1781	. . . 4
27	25	sumeq1d 6928	. . . . 5
28	25	sumeq1d 6928	. . . . . 6
29	25	sumeq1d 6928	. . . . . 6
30	28, 29	opreq12d 3963	. . . . 5
31	27, 30	eqeq12d 1481	. . . 4
32	26, 31	imbi12d 624	. . 3
33		csbopr12g 3972	. . . . . 6
34	33	adantr 389	. . . . 5
35		fsum1s 6947	. . . . . 6
36		axaddcl 5243	. . . . . . 7
37	36	r19.20si 1698	. . . . . 6
38	35, 37	sylan2 451	. . . . 5
39		fsum1s 6947	. . . . . . 7
40		pm3.26 319	. . . . . . . 8
41	40	r19.20si 1698	. . . . . . 7
42	39, 41	sylan2 451	. . . . . 6