# Metamath Proof Explorer

## Theorem fsumless

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
Hypotheses fsumge0.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumge0.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
fsumge0.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
fsumless.4 ${⊢}{\phi }\to {C}\subseteq {A}$
Assertion fsumless ${⊢}{\phi }\to \sum _{{k}\in {C}}{B}\le \sum _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 fsumge0.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fsumge0.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
3 fsumge0.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
4 fsumless.4 ${⊢}{\phi }\to {C}\subseteq {A}$
5 difss ${⊢}{A}\setminus {C}\subseteq {A}$
6 ssfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\setminus {C}\subseteq {A}\right)\to {A}\setminus {C}\in \mathrm{Fin}$
7 1 5 6 sylancl ${⊢}{\phi }\to {A}\setminus {C}\in \mathrm{Fin}$
8 eldifi ${⊢}{k}\in \left({A}\setminus {C}\right)\to {k}\in {A}$
9 8 2 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {C}\right)\right)\to {B}\in ℝ$
10 8 3 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {C}\right)\right)\to 0\le {B}$
11 7 9 10 fsumge0 ${⊢}{\phi }\to 0\le \sum _{{k}\in {A}\setminus {C}}{B}$
12 1 4 ssfid ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
13 4 sselda ${⊢}\left({\phi }\wedge {k}\in {C}\right)\to {k}\in {A}$
14 13 2 syldan ${⊢}\left({\phi }\wedge {k}\in {C}\right)\to {B}\in ℝ$
15 12 14 fsumrecl ${⊢}{\phi }\to \sum _{{k}\in {C}}{B}\in ℝ$
16 7 9 fsumrecl ${⊢}{\phi }\to \sum _{{k}\in {A}\setminus {C}}{B}\in ℝ$
17 15 16 addge01d ${⊢}{\phi }\to \left(0\le \sum _{{k}\in {A}\setminus {C}}{B}↔\sum _{{k}\in {C}}{B}\le \sum _{{k}\in {C}}{B}+\sum _{{k}\in {A}\setminus {C}}{B}\right)$
18 11 17 mpbid ${⊢}{\phi }\to \sum _{{k}\in {C}}{B}\le \sum _{{k}\in {C}}{B}+\sum _{{k}\in {A}\setminus {C}}{B}$
19 disjdif ${⊢}{C}\cap \left({A}\setminus {C}\right)=\varnothing$
20 19 a1i ${⊢}{\phi }\to {C}\cap \left({A}\setminus {C}\right)=\varnothing$
21 undif ${⊢}{C}\subseteq {A}↔{C}\cup \left({A}\setminus {C}\right)={A}$
22 4 21 sylib ${⊢}{\phi }\to {C}\cup \left({A}\setminus {C}\right)={A}$
23 22 eqcomd ${⊢}{\phi }\to {A}={C}\cup \left({A}\setminus {C}\right)$
24 2 recnd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
25 20 23 1 24 fsumsplit ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{k}\in {C}}{B}+\sum _{{k}\in {A}\setminus {C}}{B}$
26 18 25 breqtrrd ${⊢}{\phi }\to \sum _{{k}\in {C}}{B}\le \sum _{{k}\in {A}}{B}$