Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem fsumabs 6989

Description: Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values.

Assertion

Ref	Expression
fsumabs

Distinct variable groups:   ,   ,

---

Proof of Theorem fsumabs

Step	Hyp	Ref	Expression
1		opreq2 3960	. . . . 5
2	1	raleq1d 1786	. . . 4
3	1	sumeq1d 6936	. . . . . 6
4	3	fveq2d 3719	. . . . 5
5	1	sumeq1d 6936	. . . . 5
6	4, 5	breq12d 2626	. . . 4
7	2, 6	imbi12d 625	. . 3
8		opreq2 3960	. . . . 5
9	8	raleq1d 1786	. . . 4
10	8	sumeq1d 6936	. . . . . 6
11	10	fveq2d 3719	. . . . 5
12	8	sumeq1d 6936	. . . . 5
13	11, 12	breq12d 2626	. . . 4
14	9, 13	imbi12d 625	. . 3
15		opreq2 3960	. . . . 5
16	15	raleq1d 1786	. . . 4
17	15	sumeq1d 6936	. . . . . 6
18	17	fveq2d 3719	. . . . 5
19	15	sumeq1d 6936	. . . . 5
20	18, 19	breq12d 2626	. . . 4
21	16, 20	imbi12d 625	. . 3
22		opreq2 3960	. . . . 5
23	22	raleq1d 1786	. . . 4
24	22	sumeq1d 6936	. . . . . 6
25	24	fveq2d 3719	. . . . 5
26	22	sumeq1d 6936	. . . . 5
27	25, 26	breq12d 2626	. . . 4
28	23, 27	imbi12d 625	. . 3
29		csbfv2g 3734	. . . . . . 7
30	29	adantr 389	. . . . . 6
31		ra4csbela 2038	. . . . . . . 8
32		elfz3t 6431	. . . . . . . 8
33		absclt 6776	. . . . . . . . 9
34	33	r19.20si 1703	. . . . . . . 8
35	31, 32, 34	syl2an 454	. . . . . . 7
36		leidt 5512	. . . . . . 7
37	35, 36	syl 10	. . . . . 6
38	30, 37	eqbrtrrd 2632	. . . . 5
39		fsum1s 6955	. . . . . 6
40	39	fveq2d 3719	. . . . 5
41		fsum1s 6955	. . . . . 6
42	33	recnd 5295	. . . . . . 7
43	42	r19.20si 1703	. . . . . 6
44	41, 43	sylan2 451	. . . . 5
45	38, 40, 44	3brtr4d 2640	. . . 4
46	45	ex 373	. . 3
47		fzssp1t 6446	. . . . . . . . 9
48		eluzel2 6364	. . . . . . . . 9
49		eluzelz 6363	. . . . . . . . 9
50	47, 48, 49	sylanc 471	. . . . . . . 8
51	50	sseld 2063	. . . . . . 7