Theorem fsumge0

Description: If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005) (Revised by Mario Carneiro, 24-Apr-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 )
Assertion	fsumge0	|- ( ph -> 0 <_ 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		rge0ssre	|- ( 0 [,) +oo ) C_ RR
5		ax-resscn	|- RR C_ CC
6	4 5	sstri	|- ( 0 [,) +oo ) C_ CC
7	6	a1i	|- ( ph -> ( 0 [,) +oo ) C_ CC )
8		ge0addcl	|- ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
9	8	adantl	|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
10		elrege0	|- ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
11	2 3 10	sylanbrc	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
12		0e0icopnf	|- 0 e. ( 0 [,) +oo )
13	12	a1i	|- ( ph -> 0 e. ( 0 [,) +oo ) )
14	7 9 1 11 13	fsumcllem	|- ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )
15		elrege0	|- ( sum_ k e. A B e. ( 0 [,) +oo ) <-> ( sum_ k e. A B e. RR /\ 0 <_ sum_ k e. A B ) )
16	15	simprbi	|- ( sum_ k e. A B e. ( 0 [,) +oo ) -> 0 <_ sum_ k e. A B )
17	14 16	syl	|- ( ph -> 0 <_ sum_ k e. A B )