Theorem fsumge1

Description: A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 4-Jun-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$$
	fsumge1.4	$$⊢k=M\to B=C$$
	fsumge1.5	$$⊢\phi \to M\in A$$
Assertion	fsumge1	$$⊢\phi \to C\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		fsumge1.4	$$⊢k=M\to B=C$$
5		fsumge1.5	$$⊢\phi \to M\in A$$
6	4	eleq1d	$$⊢k=M\to \left(B\in ℂ\leftrightarrow C\in ℂ\right)$$
7	2	recnd	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
8	7	ralrimiva	$$⊢\phi \to \forall k\in AB\in ℂ$$
9	6 8 5	rspcdva	$$⊢\phi \to C\in ℂ$$
10	4	sumsn	$$⊢\left(M\in A\wedge C\in ℂ\right)\to \sum _{k\in \left\{M\right\}}B=C$$
11	5 9 10	syl2anc	$$⊢\phi \to \sum _{k\in \left\{M\right\}}B=C$$
12	5	snssd	$$⊢\phi \to \left\{M\right\}\subseteq A$$
13	1 2 3 12	fsumless	$$⊢\phi \to \sum _{k\in \left\{M\right\}}B\le \sum _{k\in A}B$$
14	11 13	eqbrtrrd	$$⊢\phi \to C\le \sum _{k\in A}B$$