fsum1ps - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem fsum1ps 6907

Description: Separate out the first term in a finite sum.

**Assertion**
Ref	Expression
fsum1ps	$/\$ $/\$

**Proof of Theorem fsum1ps**
Step	Hyp	Ref	Expression
1		opreq2 3908	. . . . . . 7
2	1	raleq1d 1765	. . . . . 6
3	1	sumeq1d 6879	. . . . . . 7
4		opreq2 3908	. . . . . . . . 9
5	4	sumeq1d 6879	. . . . . . . 8
6	5	opreq2d 3915	. . . . . . 7
7	3, 6	eqeq12d 1465	. . . . . 6
8	2, 7	imbi12d 624	. . . . 5
9		opreq2 3908	. . . . . . 7
10	9	raleq1d 1765	. . . . . 6
11	9	sumeq1d 6879	. . . . . . 7
12		opreq2 3908	. . . . . . . . 9
13	12	sumeq1d 6879	. . . . . . . 8
14	13	opreq2d 3915	. . . . . . 7
15	11, 14	eqeq12d 1465	. . . . . 6
16	10, 15	imbi12d 624	. . . . 5
17		opreq2 3908	. . . . . . 7
18	17	raleq1d 1765	. . . . . 6
19	17	sumeq1d 6879	. . . . . . 7
20		opreq2 3908	. . . . . . . . 9
21	20	sumeq1d 6879	. . . . . . . 8
22	21	opreq2d 3915	. . . . . . 7
23	19, 22	eqeq12d 1465	. . . . . 6
24	18, 23	imbi12d 624	. . . . 5
25		opreq2 3908	. . . . . . 7
26	25	raleq1d 1765	. . . . . 6
27	25	sumeq1d 6879	. . . . . . 7
28		opreq2 3908	. . . . . . . . 9
29	28	sumeq1d 6879	. . . . . . . 8
30	29	opreq2d 3915	. . . . . . 7
31	27, 30	eqeq12d 1465	. . . . . 6
32	26, 31	imbi12d 624	. . . . 5
33		fsump1s 6902	. . . . . . . 8 $/\$
34		uzidt 6310	. . . . . . . 8
35	33, 34	sylan 448	. . . . . . 7 $/\$
36		fzssp1t 6389	. . . . . . . . . . . . . . 15 $/\$
37	36	anidms 434	. . . . . . . . . . . . . 14
38	37	sseld 2038	. . . . . . . . . . . . 13
39	38	imim1d 28	. . . . . . . . . . . 12
40	39	r19.20dv2 1687	. . . . . . . . . . 11
41	40	imp 350	. . . . . . . . . 10 $/\$
42		fsum1s 6898	. . . . . . . . . 10 $/\$
43	41, 42	syldan 467	. . . . . . . . 9 $/\$
44	43	eqcomd 1456	. . . . . . . 8