Theorem isumsup

Description: An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014)

	Ref	Expression
Hypotheses	isumsup.1	|- Z = ( ZZ>= ` M )
	isumsup.2	|- G = seq M ( + , F )
	isumsup.3	|- ( ph -> M e. ZZ )
	isumsup.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumsup.5	|- ( ( ph /\ k e. Z ) -> A e. RR )
	isumsup.6	|- ( ( ph /\ k e. Z ) -> 0 <_ A )
	isumsup.7	|- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )
Assertion	isumsup	|- ( ph -> sum_ k e. Z A = sup ( ran G , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		isumsup.1	|- Z = ( ZZ>= ` M )
2		isumsup.2	|- G = seq M ( + , F )
3		isumsup.3	|- ( ph -> M e. ZZ )
4		isumsup.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		isumsup.5	|- ( ( ph /\ k e. Z ) -> A e. RR )
6		isumsup.6	|- ( ( ph /\ k e. Z ) -> 0 <_ A )
7		isumsup.7	|- ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )
8	5	recnd	|- ( ( ph /\ k e. Z ) -> A e. CC )
9	1 2 3 4 5 6 7	isumsup2	|- ( ph -> G ~~> sup ( ran G , RR , < ) )
10	2 9	eqbrtrrid	|- ( ph -> seq M ( + , F ) ~~> sup ( ran G , RR , < ) )
11	1 3 4 8 10	isumclim	|- ( ph -> sum_ k e. Z A = sup ( ran G , RR , < ) )