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\leftrightarrow \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\leftrightarrow 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$$