Theorem isumge0

Description: An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypotheses	isumrecl.1	|- Z = ( ZZ>= ` M )
	isumrecl.2	|- ( ph -> M e. ZZ )
	isumrecl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumrecl.4	|- ( ( ph /\ k e. Z ) -> A e. RR )
	isumrecl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
	isumge0.6	|- ( ( ph /\ k e. Z ) -> 0 <_ A )
Assertion	isumge0	|- ( ph -> 0 <_ sum_ k e. Z A )

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	|- Z = ( ZZ>= ` M )
2		isumrecl.2	|- ( ph -> M e. ZZ )
3		isumrecl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumrecl.4	|- ( ( ph /\ k e. Z ) -> A e. RR )
5		isumrecl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
6		isumge0.6	|- ( ( ph /\ k e. Z ) -> 0 <_ A )
7	4	recnd	|- ( ( ph /\ k e. Z ) -> A e. CC )
8	1 2 3 7 5	isumclim2	|- ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
9		fveq2	|- ( j = k -> ( F ` j ) = ( F ` k ) )
10	9	cbvsumv	|- sum_ j e. Z ( F ` j ) = sum_ k e. Z ( F ` k )
11	3	sumeq2dv	|- ( ph -> sum_ k e. Z ( F ` k ) = sum_ k e. Z A )
12	10 11	syl5eq	|- ( ph -> sum_ j e. Z ( F ` j ) = sum_ k e. Z A )
13	8 12	breqtrrd	|- ( ph -> seq M ( + , F ) ~~> sum_ j e. Z ( F ` j ) )
14	3 4	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
15	6 3	breqtrrd	|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
16	1 2 13 14 15	iserge0	|- ( ph -> 0 <_ sum_ j e. Z ( F ` j ) )
17	16 12	breqtrd	|- ( ph -> 0 <_ sum_ k e. Z A )