| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fsumless | Structured version Visualization version GIF version | ||
| Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
| Ref | Expression |
|---|---|
| fsumge0.1 | ⊢ (𝜑 → 𝐴 ∈ Fin) |
| fsumge0.2 | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| fsumge0.3 | ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
| fsumless.4 | ⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
| Ref | Expression |
|---|---|
| fsumless | ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsumge0.1 | . . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin) | |
| 2 | difss 4087 | . . . . 5 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴 | |
| 3 | ssfi 9134 | . . . . 5 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∖ 𝐶) ⊆ 𝐴) → (𝐴 ∖ 𝐶) ∈ Fin) | |
| 4 | 1, 2, 3 | sylancl 595 | . . . 4 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ∈ Fin) |
| 5 | eldifi 4082 | . . . . 5 ⊢ (𝑘 ∈ (𝐴 ∖ 𝐶) → 𝑘 ∈ 𝐴) | |
| 6 | fsumge0.2 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | |
| 7 | 5, 6 | sylan2 602 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ∈ ℝ) |
| 8 | fsumge0.3 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) | |
| 9 | 5, 8 | sylan2 602 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → 0 ≤ 𝐵) |
| 10 | 4, 7, 9 | fsumge0 15813 | . . 3 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵) |
| 11 | fsumless.4 | . . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ 𝐴) | |
| 12 | 1, 11 | ssfid 9206 | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ Fin) |
| 13 | 11 | sselda 3934 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ 𝐴) |
| 14 | 13, 6 | syldan 600 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ ℝ) |
| 15 | 12, 14 | fsumrecl 15751 | . . . 4 ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ∈ ℝ) |
| 16 | 4, 7 | fsumrecl 15751 | . . . 4 ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵 ∈ ℝ) |
| 17 | 15, 16 | addge01d 11768 | . . 3 ⊢ (𝜑 → (0 ≤ Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵 ↔ Σ𝑘 ∈ 𝐶 𝐵 ≤ (Σ𝑘 ∈ 𝐶 𝐵 + Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵))) |
| 18 | 10, 17 | mpbid 234 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ (Σ𝑘 ∈ 𝐶 𝐵 + Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵)) |
| 19 | disjdif 4423 | . . . 4 ⊢ (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅ | |
| 20 | 19 | a1i 11 | . . 3 ⊢ (𝜑 → (𝐶 ∩ (𝐴 ∖ 𝐶)) = ∅) |
| 21 | undif 4433 | . . . . 5 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∪ (𝐴 ∖ 𝐶)) = 𝐴) | |
| 22 | 11, 21 | sylib 220 | . . . 4 ⊢ (𝜑 → (𝐶 ∪ (𝐴 ∖ 𝐶)) = 𝐴) |
| 23 | 22 | eqcomd 2767 | . . 3 ⊢ (𝜑 → 𝐴 = (𝐶 ∪ (𝐴 ∖ 𝐶))) |
| 24 | 6 | recnd 11203 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 25 | 20, 23, 1, 24 | fsumsplit 15758 | . 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (Σ𝑘 ∈ 𝐶 𝐵 + Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵)) |
| 26 | 18, 25 | breqtrrd 5125 | 1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 class class class wbr 5097 (class class class)co 7390 Fincfn 8920 ℝcr 11065 0cc0 11066 + caddc 11069 ≤ cle 11210 Σcsu 15703 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-inf2 9589 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 ax-pre-sup 11144 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-isom 6524 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-sup 9381 df-oi 9451 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-div 11838 df-nn 12204 df-2 12273 df-3 12274 df-n0 12475 df-z 12562 df-uz 12833 df-rp 12987 df-ico 13348 df-fz 13506 df-fzo 13653 df-seq 14008 df-exp 14068 df-hash 14337 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-clim 15505 df-sum 15704 |
| This theorem is referenced by: fsumge1 15815 fsum00 15816 ovolicc2lem4 25569 fsumharmonic 27063 chtwordi 27207 chpwordi 27208 chtlepsi 27257 chtublem 27262 perfectlem2 27281 chtppilimlem1 27524 vmadivsumb 27534 rplogsumlem2 27536 rpvmasumlem 27538 dchrvmasumiflem1 27552 rplogsum 27578 dirith2 27579 mulog2sumlem2 27586 selbergb 27600 selberg2b 27603 chpdifbndlem1 27604 logdivbnd 27607 selberg3lem2 27609 pntrsumbnd 27617 pntlemf 27656 fsumiunle 32991 esumpcvgval 34335 eulerpartlemgc 34619 reprinfz1 34876 hgt750lemb 34910 fsumlessf 46113 sge0fsum 46921 sge0xaddlem1 46967 sge0seq 46980 carageniuncllem2 47056 perfectALTVlem2 48304 |
| Copyright terms: Public domain | W3C validator |