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 φ A Fin
fsumabs.2 φ k A B
Assertion fsumabs φ k A B k A B

Proof

Step Hyp Ref Expression
1 fsumabs.1 φ A Fin
2 fsumabs.2 φ k A B
3 ssid A A
4 sseq1 w = w A A
5 sumeq1 w = k w B = k B
6 5 fveq2d w = k w B = k B
7 sumeq1 w = k w B = k B
8 6 7 breq12d w = k w B k w B k B k B
9 4 8 imbi12d w = w A k w B k w B A k B k B
10 9 imbi2d w = φ w A k w B k w B φ A k B k B
11 sseq1 w = x w A x A
12 sumeq1 w = x k w B = k x B
13 12 fveq2d w = x k w B = k x B
14 sumeq1 w = x k w B = k x B
15 13 14 breq12d w = x k w B k w B k x B k x B
16 11 15 imbi12d w = x w A k w B k w B x A k x B k x B
17 16 imbi2d w = x φ w A k w B k w B φ x A k x B k x B
18 sseq1 w = x y w A x y A
19 sumeq1 w = x y k w B = k x y B
20 19 fveq2d w = x y k w B = k x y B
21 sumeq1 w = x y k w B = k x y B
22 20 21 breq12d w = x y k w B k w B k x y B k x y B
23 18 22 imbi12d w = x y w A k w B k w B x y A k x y B k x y B
24 23 imbi2d w = x y φ w A k w B k w B φ x y A k x y B k x y B
25 sseq1 w = A w A A A
26 sumeq1 w = A k w B = k A B
27 26 fveq2d w = A k w B = k A B
28 sumeq1 w = A k w B = k A B
29 27 28 breq12d w = A k w B k w B k A B k A B
30 25 29 imbi12d w = A w A k w B k w B A A k A B k A B
31 30 imbi2d w = A φ w A k w B k w B φ A A k A B k A B
32 0le0 0 0
33 sum0 k B = 0
34 33 fveq2i k B = 0
35 abs0 0 = 0
36 34 35 eqtri k B = 0
37 sum0 k B = 0
38 32 36 37 3brtr4i k B k B
39 38 2a1i φ A k B k B
40 ssun1 x x y
41 sstr x x y x y A x A
42 40 41 mpan x y A x A
43 42 imim1i x A k x B k x B x y A k x B k x B
44 simpll φ ¬ y x x y A φ
45 44 1 syl φ ¬ y x x y A A Fin
46 simpr φ ¬ y x x y A x y A
47 46 unssad φ ¬ y x x y A x A
48 45 47 ssfid φ ¬ y x x y A x Fin
49 47 sselda φ ¬ y x x y A k x k A
50 44 49 2 syl2an2r φ ¬ y x x y A k x B
51 48 50 fsumcl φ ¬ y x x y A k x B
52 51 abscld φ ¬ y x x y A k x B
53 50 abscld φ ¬ y x x y A k x B
54 48 53 fsumrecl φ ¬ y x x y A k x B
55 46 unssbd φ ¬ y x x y A y A
56 vex y V
57 56 snss y A y A
58 55 57 sylibr φ ¬ y x x y A y A
59 2 ralrimiva φ k A B
60 44 59 syl φ ¬ y x x y A k A B
61 nfcsb1v _ k y / k B
62 61 nfel1 k y / k B
63 csbeq1a k = y B = y / k B
64 63 eleq1d k = y B y / k B
65 62 64 rspc y A k A B y / k B
66 58 60 65 sylc φ ¬ y x x y A y / k B
67 66 abscld φ ¬ y x x y A y / k B
68 52 54 67 leadd1d φ ¬ y x x y A k x B k x B k x B + y / k B k x B + y / k B
69 simplr φ ¬ y x x y A ¬ y x
70 disjsn x y = ¬ y x
71 69 70 sylibr φ ¬ y x x y A x y =
72 eqidd φ ¬ y x x y A x y = x y
73 45 46 ssfid φ ¬ y x x y A x y Fin
74 46 sselda φ ¬ y x x y A k x y k A
75 44 74 2 syl2an2r φ ¬ y x x y A k x y B
76 75 abscld φ ¬ y x x y A k x y B
77 76 recnd φ ¬ y x x y A k x y B
78 71 72 73 77 fsumsplit φ ¬ y x x y A k x y B = k x B + k y B
79 csbfv2g y V y / k B = y / k B
80 79 elv y / k B = y / k B
81 67 recnd φ ¬ y x x y A y / k B
82 80 81 eqeltrid φ ¬ y x x y A y / k B
83 sumsns y V y / k B k y B = y / k B
84 56 82 83 sylancr φ ¬ y x x y A k y B = y / k B
85 84 80 eqtrdi φ ¬ y x x y A k y B = y / k B
86 85 oveq2d φ ¬ y x x y A k x B + k y B = k x B + y / k B
87 78 86 eqtrd φ ¬ y x x y A k x y B = k x B + y / k B
88 87 breq2d φ ¬ y x x y A k x B + y / k B k x y B k x B + y / k B k x B + y / k B
89 68 88 bitr4d φ ¬ y x x y A k x B k x B k x B + y / k B k x y B
90 71 72 73 75 fsumsplit φ ¬ y x x y A k x y B = k x B + k y B
91 sumsns y A y / k B k y B = y / k B
92 58 66 91 syl2anc φ ¬ y x x y A k y B = y / k B
93 92 oveq2d φ ¬ y x x y A k x B + k y B = k x B + y / k B
94 90 93 eqtrd φ ¬ y x x y A k x y B = k x B + y / k B
95 94 fveq2d φ ¬ y x x y A k x y B = k x B + y / k B
96 51 66 abstrid φ ¬ y x x y A k x B + y / k B k x B + y / k B
97 95 96 eqbrtrd φ ¬ y x x y A k x y B k x B + y / k B
98 73 75 fsumcl φ ¬ y x x y A k x y B
99 98 abscld φ ¬ y x x y A k x y B
100 52 67 readdcld φ ¬ y x x y A k x B + y / k B
101 73 76 fsumrecl φ ¬ y x x y A k x y B
102 letr k x y B k x B + y / k B k x y B k x y B k x B + y / k B k x B + y / k B k x y B k x y B k x y B
103 99 100 101 102 syl3anc φ ¬ y x x y A k x y B k x B + y / k B k x B + y / k B k x y B k x y B k x y B
104 97 103 mpand φ ¬ y x x y A k x B + y / k B k x y B k x y B k x y B
105 89 104 sylbid φ ¬ y x x y A k x B k x B k x y B k x y B
106 105 ex φ ¬ y x x y A k x B k x B k x y B k x y B
107 106 a2d φ ¬ y x x y A k x B k x B x y A k x y B k x y B
108 43 107 syl5 φ ¬ y x x A k x B k x B x y A k x y B k x y B
109 108 expcom ¬ y x φ x A k x B k x B x y A k x y B k x y B
110 109 a2d ¬ y x φ x A k x B k x B φ x y A k x y B k x y B
111 110 adantl x Fin ¬ y x φ x A k x B k x B φ x y A k x y B k x y B
112 10 17 24 31 39 111 findcard2s A Fin φ A A k A B k A B
113 1 112 mpcom φ A A k A B k A B
114 3 113 mpi φ k A B k A B