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	|- ( ph -> A e. Fin )
	fsumge0.2	|- ( ( ph /\ k e. A ) -> B e. RR )
	fsumge0.3	|- ( ( ph /\ k e. A ) -> 0 <_ B )
	fsumge1.4	|- ( k = M -> B = C )
	fsumge1.5	|- ( ph -> M e. A )
Assertion	fsumge1	|- ( ph -> C <_ sum_ k e. A B )

Proof

Step	Hyp	Ref	Expression
1		fsumge0.1	|- ( ph -> A e. Fin )
2		fsumge0.2	|- ( ( ph /\ k e. A ) -> B e. RR )
3		fsumge0.3	|- ( ( ph /\ k e. A ) -> 0 <_ B )
4		fsumge1.4	|- ( k = M -> B = C )
5		fsumge1.5	|- ( ph -> M e. A )
6	4	eleq1d	|- ( k = M -> ( B e. CC <-> C e. CC ) )
7	2	recnd	|- ( ( ph /\ k e. A ) -> B e. CC )
8	7	ralrimiva	|- ( ph -> A. k e. A B e. CC )
9	6 8 5	rspcdva	|- ( ph -> C e. CC )
10	4	sumsn	|- ( ( M e. A /\ C e. CC ) -> sum_ k e. { M } B = C )
11	5 9 10	syl2anc	|- ( ph -> sum_ k e. { M } B = C )
12	5	snssd	|- ( ph -> { M } C_ A )
13	1 2 3 12	fsumless	|- ( ph -> sum_ k e. { M } B <_ sum_ k e. A B )
14	11 13	eqbrtrrd	|- ( ph -> C <_ sum_ k e. A B )