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
|- ( ph -> A e. Fin )
fsumabs.2
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumabs
|- ( ph -> ( abs ` sum_ k e. A B ) <_ sum_ k e. A ( abs ` B ) )

Proof

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