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