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={\mathbb{Z}}_{\ge M}$$
	isumsup.2	$$⊢G=seqM\left(+,F\right)$$
	isumsup.3	$$⊢\phi \to M\in \mathbb{Z}$$
	isumsup.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumsup.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
	isumsup.6	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le A$$
	isumsup.7	$$⊢\phi \to \exists x\in ℝ\forall j\in ZG\left(j\right)\le x$$
Assertion	isumsup	$$⊢\phi \to \sum _{k\in Z}A=sup\left(\mathrm{ran}G,ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		isumsup.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumsup.2	$$⊢G=seqM\left(+,F\right)$$
3		isumsup.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		isumsup.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		isumsup.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
6		isumsup.6	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le A$$
7		isumsup.7	$$⊢\phi \to \exists x\in ℝ\forall j\in ZG\left(j\right)\le x$$
8	5	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
9	1 2 3 4 5 6 7	isumsup2	$$⊢\phi \to G⇝sup\left(\mathrm{ran}G,ℝ,<\right)$$
10	2 9	eqbrtrrid	$$⊢\phi \to seqM\left(+,F\right)⇝sup\left(\mathrm{ran}G,ℝ,<\right)$$
11	1 3 4 8 10	isumclim	$$⊢\phi \to \sum _{k\in Z}A=sup\left(\mathrm{ran}G,ℝ,<\right)$$