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 ) )