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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumabs.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsumabs ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ≤ Σ 𝑘 ∈ 𝐴 ( abs ‘ 𝐵 ) )

Proof

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