Theorem iserge0

Description: The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	|- Z = ( ZZ>= ` M )
2		iserge0.2	|- ( ph -> M e. ZZ )
3		iserge0.3	|- ( ph -> seq M ( + , F ) ~~> A )
4		iserge0.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5		iserge0.5	|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
6		serclim0	|- ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
7	2 6	syl	|- ( ph -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
8		simpr	|- ( ( ph /\ k e. Z ) -> k e. Z )
9	8 1	eleqtrdi	|- ( ( ph /\ k e. Z ) -> k e. ( ZZ>= ` M ) )
10		c0ex	|- 0 e. _V
11	10	fvconst2	|- ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = 0 )
12	9 11	syl	|- ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = 0 )
13		0re	|- 0 e. RR
14	12 13	eqeltrdi	|- ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) e. RR )
15	12 5	eqbrtrd	|- ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) <_ ( F ` k ) )
16	1 2 7 3 14 4 15	iserle	|- ( ph -> 0 <_ A )