Metamath Proof Explorer


Theorem fsumabs

Description: Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by NM, 9-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumabs.1 φAFin
fsumabs.2 φkAB
Assertion fsumabs φkABkAB

Proof

Step Hyp Ref Expression
1 fsumabs.1 φAFin
2 fsumabs.2 φkAB
3 ssid AA
4 sseq1 w=wAA
5 sumeq1 w=kwB=kB
6 5 fveq2d w=kwB=kB
7 sumeq1 w=kwB=kB
8 6 7 breq12d w=kwBkwBkBkB
9 4 8 imbi12d w=wAkwBkwBAkBkB
10 9 imbi2d w=φwAkwBkwBφAkBkB
11 sseq1 w=xwAxA
12 sumeq1 w=xkwB=kxB
13 12 fveq2d w=xkwB=kxB
14 sumeq1 w=xkwB=kxB
15 13 14 breq12d w=xkwBkwBkxBkxB
16 11 15 imbi12d w=xwAkwBkwBxAkxBkxB
17 16 imbi2d w=xφwAkwBkwBφxAkxBkxB
18 sseq1 w=xywAxyA
19 sumeq1 w=xykwB=kxyB
20 19 fveq2d w=xykwB=kxyB
21 sumeq1 w=xykwB=kxyB
22 20 21 breq12d w=xykwBkwBkxyBkxyB
23 18 22 imbi12d w=xywAkwBkwBxyAkxyBkxyB
24 23 imbi2d w=xyφwAkwBkwBφxyAkxyBkxyB
25 sseq1 w=AwAAA
26 sumeq1 w=AkwB=kAB
27 26 fveq2d w=AkwB=kAB
28 sumeq1 w=AkwB=kAB
29 27 28 breq12d w=AkwBkwBkABkAB
30 25 29 imbi12d w=AwAkwBkwBAAkABkAB
31 30 imbi2d w=AφwAkwBkwBφAAkABkAB
32 0le0 00
33 sum0 kB=0
34 33 fveq2i kB=0
35 abs0 0=0
36 34 35 eqtri kB=0
37 sum0 kB=0
38 32 36 37 3brtr4i kBkB
39 38 2a1i φAkBkB
40 ssun1 xxy
41 sstr xxyxyAxA
42 40 41 mpan xyAxA
43 42 imim1i xAkxBkxBxyAkxBkxB
44 simpll φ¬yxxyAφ
45 44 1 syl φ¬yxxyAAFin
46 simpr φ¬yxxyAxyA
47 46 unssad φ¬yxxyAxA
48 45 47 ssfid φ¬yxxyAxFin
49 47 sselda φ¬yxxyAkxkA
50 44 49 2 syl2an2r φ¬yxxyAkxB
51 48 50 fsumcl φ¬yxxyAkxB
52 51 abscld φ¬yxxyAkxB
53 50 abscld φ¬yxxyAkxB
54 48 53 fsumrecl φ¬yxxyAkxB
55 46 unssbd φ¬yxxyAyA
56 vex yV
57 56 snss yAyA
58 55 57 sylibr φ¬yxxyAyA
59 2 ralrimiva φkAB
60 44 59 syl φ¬yxxyAkAB
61 nfcsb1v _ky/kB
62 61 nfel1 ky/kB
63 csbeq1a k=yB=y/kB
64 63 eleq1d k=yBy/kB
65 62 64 rspc yAkABy/kB
66 58 60 65 sylc φ¬yxxyAy/kB
67 66 abscld φ¬yxxyAy/kB
68 52 54 67 leadd1d φ¬yxxyAkxBkxBkxB+y/kBkxB+y/kB
69 simplr φ¬yxxyA¬yx
70 disjsn xy=¬yx
71 69 70 sylibr φ¬yxxyAxy=
72 eqidd φ¬yxxyAxy=xy
73 45 46 ssfid φ¬yxxyAxyFin
74 46 sselda φ¬yxxyAkxykA
75 44 74 2 syl2an2r φ¬yxxyAkxyB
76 75 abscld φ¬yxxyAkxyB
77 76 recnd φ¬yxxyAkxyB
78 71 72 73 77 fsumsplit φ¬yxxyAkxyB=kxB+kyB
79 csbfv2g yVy/kB=y/kB
80 79 elv y/kB=y/kB
81 67 recnd φ¬yxxyAy/kB
82 80 81 eqeltrid φ¬yxxyAy/kB
83 sumsns yVy/kBkyB=y/kB
84 56 82 83 sylancr φ¬yxxyAkyB=y/kB
85 84 80 eqtrdi φ¬yxxyAkyB=y/kB
86 85 oveq2d φ¬yxxyAkxB+kyB=kxB+y/kB
87 78 86 eqtrd φ¬yxxyAkxyB=kxB+y/kB
88 87 breq2d φ¬yxxyAkxB+y/kBkxyBkxB+y/kBkxB+y/kB
89 68 88 bitr4d φ¬yxxyAkxBkxBkxB+y/kBkxyB
90 71 72 73 75 fsumsplit φ¬yxxyAkxyB=kxB+kyB
91 sumsns yAy/kBkyB=y/kB
92 58 66 91 syl2anc φ¬yxxyAkyB=y/kB
93 92 oveq2d φ¬yxxyAkxB+kyB=kxB+y/kB
94 90 93 eqtrd φ¬yxxyAkxyB=kxB+y/kB
95 94 fveq2d φ¬yxxyAkxyB=kxB+y/kB
96 51 66 abstrid φ¬yxxyAkxB+y/kBkxB+y/kB
97 95 96 eqbrtrd φ¬yxxyAkxyBkxB+y/kB
98 73 75 fsumcl φ¬yxxyAkxyB
99 98 abscld φ¬yxxyAkxyB
100 52 67 readdcld φ¬yxxyAkxB+y/kB
101 73 76 fsumrecl φ¬yxxyAkxyB
102 letr kxyBkxB+y/kBkxyBkxyBkxB+y/kBkxB+y/kBkxyBkxyBkxyB
103 99 100 101 102 syl3anc φ¬yxxyAkxyBkxB+y/kBkxB+y/kBkxyBkxyBkxyB
104 97 103 mpand φ¬yxxyAkxB+y/kBkxyBkxyBkxyB
105 89 104 sylbid φ¬yxxyAkxBkxBkxyBkxyB
106 105 ex φ¬yxxyAkxBkxBkxyBkxyB
107 106 a2d φ¬yxxyAkxBkxBxyAkxyBkxyB
108 43 107 syl5 φ¬yxxAkxBkxBxyAkxyBkxyB
109 108 expcom ¬yxφxAkxBkxBxyAkxyBkxyB
110 109 a2d ¬yxφxAkxBkxBφxyAkxyBkxyB
111 110 adantl xFin¬yxφxAkxBkxBφxyAkxyBkxyB
112 10 17 24 31 39 111 findcard2s AFinφAAkABkAB
113 1 112 mpcom φAAkABkAB
114 3 113 mpi φkABkAB