MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumabs Structured version   Visualization version   GIF version

Theorem fsumabs 15693
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.)
Hypotheses
Ref Expression
fsumabs.1 (𝜑𝐴 ∈ Fin)
fsumabs.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
Assertion
Ref Expression
fsumabs (𝜑 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵))
Distinct variable groups:   𝐴,𝑘   𝜑,𝑘
Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem fsumabs
Dummy variables 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3971 . 2 𝐴𝐴
2 fsumabs.1 . . 3 (𝜑𝐴 ∈ Fin)
3 sseq1 3974 . . . . . 6 (𝑤 = ∅ → (𝑤𝐴 ↔ ∅ ⊆ 𝐴))
4 sumeq1 15580 . . . . . . . 8 (𝑤 = ∅ → Σ𝑘𝑤 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
54fveq2d 6851 . . . . . . 7 (𝑤 = ∅ → (abs‘Σ𝑘𝑤 𝐵) = (abs‘Σ𝑘 ∈ ∅ 𝐵))
6 sumeq1 15580 . . . . . . 7 (𝑤 = ∅ → Σ𝑘𝑤 (abs‘𝐵) = Σ𝑘 ∈ ∅ (abs‘𝐵))
75, 6breq12d 5123 . . . . . 6 (𝑤 = ∅ → ((abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵) ↔ (abs‘Σ𝑘 ∈ ∅ 𝐵) ≤ Σ𝑘 ∈ ∅ (abs‘𝐵)))
83, 7imbi12d 345 . . . . 5 (𝑤 = ∅ → ((𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵)) ↔ (∅ ⊆ 𝐴 → (abs‘Σ𝑘 ∈ ∅ 𝐵) ≤ Σ𝑘 ∈ ∅ (abs‘𝐵))))
98imbi2d 341 . . . 4 (𝑤 = ∅ → ((𝜑 → (𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵))) ↔ (𝜑 → (∅ ⊆ 𝐴 → (abs‘Σ𝑘 ∈ ∅ 𝐵) ≤ Σ𝑘 ∈ ∅ (abs‘𝐵)))))
10 sseq1 3974 . . . . . 6 (𝑤 = 𝑥 → (𝑤𝐴𝑥𝐴))
11 sumeq1 15580 . . . . . . . 8 (𝑤 = 𝑥 → Σ𝑘𝑤 𝐵 = Σ𝑘𝑥 𝐵)
1211fveq2d 6851 . . . . . . 7 (𝑤 = 𝑥 → (abs‘Σ𝑘𝑤 𝐵) = (abs‘Σ𝑘𝑥 𝐵))
13 sumeq1 15580 . . . . . . 7 (𝑤 = 𝑥 → Σ𝑘𝑤 (abs‘𝐵) = Σ𝑘𝑥 (abs‘𝐵))
1412, 13breq12d 5123 . . . . . 6 (𝑤 = 𝑥 → ((abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵) ↔ (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)))
1510, 14imbi12d 345 . . . . 5 (𝑤 = 𝑥 → ((𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵)) ↔ (𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵))))
1615imbi2d 341 . . . 4 (𝑤 = 𝑥 → ((𝜑 → (𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵))) ↔ (𝜑 → (𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)))))
17 sseq1 3974 . . . . . 6 (𝑤 = (𝑥 ∪ {𝑦}) → (𝑤𝐴 ↔ (𝑥 ∪ {𝑦}) ⊆ 𝐴))
18 sumeq1 15580 . . . . . . . 8 (𝑤 = (𝑥 ∪ {𝑦}) → Σ𝑘𝑤 𝐵 = Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵)
1918fveq2d 6851 . . . . . . 7 (𝑤 = (𝑥 ∪ {𝑦}) → (abs‘Σ𝑘𝑤 𝐵) = (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵))
20 sumeq1 15580 . . . . . . 7 (𝑤 = (𝑥 ∪ {𝑦}) → Σ𝑘𝑤 (abs‘𝐵) = Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵))
2119, 20breq12d 5123 . . . . . 6 (𝑤 = (𝑥 ∪ {𝑦}) → ((abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵) ↔ (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
2217, 21imbi12d 345 . . . . 5 (𝑤 = (𝑥 ∪ {𝑦}) → ((𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵)) ↔ ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵))))
2322imbi2d 341 . . . 4 (𝑤 = (𝑥 ∪ {𝑦}) → ((𝜑 → (𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵))) ↔ (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))))
24 sseq1 3974 . . . . . 6 (𝑤 = 𝐴 → (𝑤𝐴𝐴𝐴))
25 sumeq1 15580 . . . . . . . 8 (𝑤 = 𝐴 → Σ𝑘𝑤 𝐵 = Σ𝑘𝐴 𝐵)
2625fveq2d 6851 . . . . . . 7 (𝑤 = 𝐴 → (abs‘Σ𝑘𝑤 𝐵) = (abs‘Σ𝑘𝐴 𝐵))
27 sumeq1 15580 . . . . . . 7 (𝑤 = 𝐴 → Σ𝑘𝑤 (abs‘𝐵) = Σ𝑘𝐴 (abs‘𝐵))
2826, 27breq12d 5123 . . . . . 6 (𝑤 = 𝐴 → ((abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵) ↔ (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵)))
2924, 28imbi12d 345 . . . . 5 (𝑤 = 𝐴 → ((𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵)) ↔ (𝐴𝐴 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵))))
3029imbi2d 341 . . . 4 (𝑤 = 𝐴 → ((𝜑 → (𝑤𝐴 → (abs‘Σ𝑘𝑤 𝐵) ≤ Σ𝑘𝑤 (abs‘𝐵))) ↔ (𝜑 → (𝐴𝐴 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵)))))
31 0le0 12261 . . . . . 6 0 ≤ 0
32 sum0 15613 . . . . . . . 8 Σ𝑘 ∈ ∅ 𝐵 = 0
3332fveq2i 6850 . . . . . . 7 (abs‘Σ𝑘 ∈ ∅ 𝐵) = (abs‘0)
34 abs0 15177 . . . . . . 7 (abs‘0) = 0
3533, 34eqtri 2765 . . . . . 6 (abs‘Σ𝑘 ∈ ∅ 𝐵) = 0
36 sum0 15613 . . . . . 6 Σ𝑘 ∈ ∅ (abs‘𝐵) = 0
3731, 35, 363brtr4i 5140 . . . . 5 (abs‘Σ𝑘 ∈ ∅ 𝐵) ≤ Σ𝑘 ∈ ∅ (abs‘𝐵)
38372a1i 12 . . . 4 (𝜑 → (∅ ⊆ 𝐴 → (abs‘Σ𝑘 ∈ ∅ 𝐵) ≤ Σ𝑘 ∈ ∅ (abs‘𝐵)))
39 ssun1 4137 . . . . . . . . . 10 𝑥 ⊆ (𝑥 ∪ {𝑦})
40 sstr 3957 . . . . . . . . . 10 ((𝑥 ⊆ (𝑥 ∪ {𝑦}) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥𝐴)
4139, 40mpan 689 . . . . . . . . 9 ((𝑥 ∪ {𝑦}) ⊆ 𝐴𝑥𝐴)
4241imim1i 63 . . . . . . . 8 ((𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)))
43 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝜑)
4443, 2syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝐴 ∈ Fin)
45 simpr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
4645unssad 4152 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥𝐴)
4744, 46ssfid 9218 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑥 ∈ Fin)
4846sselda 3949 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘𝑥) → 𝑘𝐴)
49 fsumabs.2 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
5043, 48, 49syl2an2r 684 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘𝑥) → 𝐵 ∈ ℂ)
5147, 50fsumcl 15625 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘𝑥 𝐵 ∈ ℂ)
5251abscld 15328 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘Σ𝑘𝑥 𝐵) ∈ ℝ)
5350abscld 15328 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘𝑥) → (abs‘𝐵) ∈ ℝ)
5447, 53fsumrecl 15626 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘𝑥 (abs‘𝐵) ∈ ℝ)
5545unssbd 4153 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴)
56 vex 3452 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
5756snss 4751 . . . . . . . . . . . . . . . 16 (𝑦𝐴 ↔ {𝑦} ⊆ 𝐴)
5855, 57sylibr 233 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑦𝐴)
5949ralrimiva 3144 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
6043, 59syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ∀𝑘𝐴 𝐵 ∈ ℂ)
61 nfcsb1v 3885 . . . . . . . . . . . . . . . . 17 𝑘𝑦 / 𝑘𝐵
6261nfel1 2924 . . . . . . . . . . . . . . . 16 𝑘𝑦 / 𝑘𝐵 ∈ ℂ
63 csbeq1a 3874 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦𝐵 = 𝑦 / 𝑘𝐵)
6463eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (𝐵 ∈ ℂ ↔ 𝑦 / 𝑘𝐵 ∈ ℂ))
6562, 64rspc 3572 . . . . . . . . . . . . . . 15 (𝑦𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑦 / 𝑘𝐵 ∈ ℂ))
6658, 60, 65sylc 65 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 / 𝑘𝐵 ∈ ℂ)
6766abscld 15328 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘𝑦 / 𝑘𝐵) ∈ ℝ)
6852, 54, 67leadd1d 11756 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ((abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵) ↔ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ (Σ𝑘𝑥 (abs‘𝐵) + (abs‘𝑦 / 𝑘𝐵))))
69 simplr 768 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ¬ 𝑦𝑥)
70 disjsn 4677 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝑥)
7169, 70sylibr 233 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∩ {𝑦}) = ∅)
72 eqidd 2738 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
7344, 45ssfid 9218 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (𝑥 ∪ {𝑦}) ∈ Fin)
7445sselda 3949 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘 ∈ (𝑥 ∪ {𝑦})) → 𝑘𝐴)
7543, 74, 49syl2an2r 684 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ ℂ)
7675abscld 15328 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘 ∈ (𝑥 ∪ {𝑦})) → (abs‘𝐵) ∈ ℝ)
7776recnd 11190 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑘 ∈ (𝑥 ∪ {𝑦})) → (abs‘𝐵) ∈ ℂ)
7871, 72, 73, 77fsumsplit 15633 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) = (Σ𝑘𝑥 (abs‘𝐵) + Σ𝑘 ∈ {𝑦} (abs‘𝐵)))
79 csbfv2g 6896 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ V → 𝑦 / 𝑘(abs‘𝐵) = (abs‘𝑦 / 𝑘𝐵))
8079elv 3454 . . . . . . . . . . . . . . . . . 18 𝑦 / 𝑘(abs‘𝐵) = (abs‘𝑦 / 𝑘𝐵)
8167recnd 11190 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘𝑦 / 𝑘𝐵) ∈ ℂ)
8280, 81eqeltrid 2842 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 / 𝑘(abs‘𝐵) ∈ ℂ)
83 sumsns 15642 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ V ∧ 𝑦 / 𝑘(abs‘𝐵) ∈ ℂ) → Σ𝑘 ∈ {𝑦} (abs‘𝐵) = 𝑦 / 𝑘(abs‘𝐵))
8456, 82, 83sylancr 588 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ {𝑦} (abs‘𝐵) = 𝑦 / 𝑘(abs‘𝐵))
8584, 80eqtrdi 2793 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ {𝑦} (abs‘𝐵) = (abs‘𝑦 / 𝑘𝐵))
8685oveq2d 7378 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (Σ𝑘𝑥 (abs‘𝐵) + Σ𝑘 ∈ {𝑦} (abs‘𝐵)) = (Σ𝑘𝑥 (abs‘𝐵) + (abs‘𝑦 / 𝑘𝐵)))
8778, 86eqtrd 2777 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) = (Σ𝑘𝑥 (abs‘𝐵) + (abs‘𝑦 / 𝑘𝐵)))
8887breq2d 5122 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) ↔ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ (Σ𝑘𝑥 (abs‘𝐵) + (abs‘𝑦 / 𝑘𝐵))))
8968, 88bitr4d 282 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ((abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵) ↔ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
9071, 72, 73, 75fsumsplit 15633 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵 = (Σ𝑘𝑥 𝐵 + Σ𝑘 ∈ {𝑦}𝐵))
91 sumsns 15642 . . . . . . . . . . . . . . . . 17 ((𝑦𝐴𝑦 / 𝑘𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝑦}𝐵 = 𝑦 / 𝑘𝐵)
9258, 66, 91syl2anc 585 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ {𝑦}𝐵 = 𝑦 / 𝑘𝐵)
9392oveq2d 7378 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (Σ𝑘𝑥 𝐵 + Σ𝑘 ∈ {𝑦}𝐵) = (Σ𝑘𝑥 𝐵 + 𝑦 / 𝑘𝐵))
9490, 93eqtrd 2777 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵 = (Σ𝑘𝑥 𝐵 + 𝑦 / 𝑘𝐵))
9594fveq2d 6851 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) = (abs‘(Σ𝑘𝑥 𝐵 + 𝑦 / 𝑘𝐵)))
9651, 66abstrid 15348 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘(Σ𝑘𝑥 𝐵 + 𝑦 / 𝑘𝐵)) ≤ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)))
9795, 96eqbrtrd 5132 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)))
9873, 75fsumcl 15625 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵 ∈ ℂ)
9998abscld 15328 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ∈ ℝ)
10052, 67readdcld 11191 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ∈ ℝ)
10173, 76fsumrecl 15626 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) ∈ ℝ)
102 letr 11256 . . . . . . . . . . . . 13 (((abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ∈ ℝ ∧ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ∈ ℝ ∧ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) ∈ ℝ) → (((abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ∧ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
10399, 100, 101, 102syl3anc 1372 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (((abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ∧ ((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
10497, 103mpand 694 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → (((abs‘Σ𝑘𝑥 𝐵) + (abs‘𝑦 / 𝑘𝐵)) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
10589, 104sylbid 239 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝑦𝑥) ∧ (𝑥 ∪ {𝑦}) ⊆ 𝐴) → ((abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))
106105ex 414 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑦𝑥) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → ((abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵) → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵))))
107106a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑦𝑥) → (((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵))))
10842, 107syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑦𝑥) → ((𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵))))
109108expcom 415 . . . . . 6 𝑦𝑥 → (𝜑 → ((𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵)) → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))))
110109a2d 29 . . . . 5 𝑦𝑥 → ((𝜑 → (𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵))) → (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))))
111110adantl 483 . . . 4 ((𝑥 ∈ Fin ∧ ¬ 𝑦𝑥) → ((𝜑 → (𝑥𝐴 → (abs‘Σ𝑘𝑥 𝐵) ≤ Σ𝑘𝑥 (abs‘𝐵))) → (𝜑 → ((𝑥 ∪ {𝑦}) ⊆ 𝐴 → (abs‘Σ𝑘 ∈ (𝑥 ∪ {𝑦})𝐵) ≤ Σ𝑘 ∈ (𝑥 ∪ {𝑦})(abs‘𝐵)))))
1129, 16, 23, 30, 38, 111findcard2s 9116 . . 3 (𝐴 ∈ Fin → (𝜑 → (𝐴𝐴 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵))))
1132, 112mpcom 38 . 2 (𝜑 → (𝐴𝐴 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵)))
1141, 113mpi 20 1 (𝜑 → (abs‘Σ𝑘𝐴 𝐵) ≤ Σ𝑘𝐴 (abs‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  wral 3065  Vcvv 3448  csb 3860  cun 3913  cin 3914  wss 3915  c0 4287  {csn 4591   class class class wbr 5110  cfv 6501  (class class class)co 7362  Fincfn 8890  cc 11056  cr 11057  0cc0 11058   + caddc 11061  cle 11197  abscabs 15126  Σcsu 15577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578
This theorem is referenced by:  o1fsum  15705  seqabs  15706  cvgcmpce  15710  mertenslem1  15776  dvfsumabs  25403  mtest  25779  mtestbdd  25780  abelthlem7  25813  fsumharmonic  26377  ftalem1  26438  ftalem5  26442  dchrisumlem2  26854  dchrmusum2  26858  dchrvmasumlem3  26863  dchrvmasumiflem1  26865  dchrisum0lem1  26880  dchrisum0lem2a  26881  mudivsum  26894  mulogsumlem  26895  2vmadivsumlem  26904  selberglem2  26910  selberg3lem1  26921  selberg4lem1  26924  pntrsumbnd  26930  pntrlog2bndlem1  26941  pntrlog2bndlem3  26943  knoppndvlem11  35014  fourierdlem73  44494  etransclem23  44572
  Copyright terms: Public domain W3C validator