| 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 9135 | . . . . 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 15814 | . . 3 ⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵) |
| 11 | fsumless.4 | . . . . . 6 ⊢ (𝜑 → 𝐶 ⊆ 𝐴) | |
| 12 | 1, 11 | ssfid 9207 | . . . . 5 ⊢ (𝜑 → 𝐶 ∈ Fin) |
| 13 | 11 | sselda 3934 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ 𝐴) |
| 14 | 13, 6 | syldan 600 | . . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ ℝ) |
| 15 | 12, 14 | fsumrecl 15752 | . . . 4 ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ∈ ℝ) |
| 16 | 4, 7 | fsumrecl 15752 | . . . 4 ⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ 𝐶)𝐵 ∈ ℝ) |
| 17 | 15, 16 | addge01d 11769 | . . 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 11204 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 25 | 20, 23, 1, 24 | fsumsplit 15759 | . 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 7391 Fincfn 8921 ℝcr 11066 0cc0 11067 + caddc 11070 ≤ cle 11211 Σcsu 15704 |
| 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 7713 ax-inf2 9590 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145 |
| 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 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9382 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-z 12563 df-uz 12834 df-rp 12988 df-ico 13349 df-fz 13507 df-fzo 13654 df-seq 14009 df-exp 14069 df-hash 14338 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-clim 15506 df-sum 15705 |
| This theorem is referenced by: fsumge1 15816 fsum00 15817 ovolicc2lem4 25570 fsumharmonic 27064 chtwordi 27208 chpwordi 27209 chtlepsi 27258 chtublem 27263 perfectlem2 27282 chtppilimlem1 27525 vmadivsumb 27535 rplogsumlem2 27537 rpvmasumlem 27539 dchrvmasumiflem1 27553 rplogsum 27579 dirith2 27580 mulog2sumlem2 27587 selbergb 27601 selberg2b 27604 chpdifbndlem1 27605 logdivbnd 27608 selberg3lem2 27610 pntrsumbnd 27618 pntlemf 27657 fsumiunle 32992 esumpcvgval 34336 eulerpartlemgc 34620 reprinfz1 34877 hgt750lemb 34911 fsumlessf 46114 sge0fsum 46922 sge0xaddlem1 46968 sge0seq 46981 carageniuncllem2 47057 perfectALTVlem2 48305 |
| Copyright terms: Public domain | W3C validator |