Theorem isumge0

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

	Ref	Expression
Hypotheses	isumrecl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	isumrecl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumrecl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
	isumrecl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
	isumge0.6	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le A$$
Assertion	isumge0	$$⊢\phi \to 0\le \sum _{k\in Z}A$$

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumrecl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumrecl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isumrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
5		isumrecl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6		isumge0.6	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le A$$
7	4	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
8	1 2 3 7 5	isumclim2	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{k\in Z}A$$
9		fveq2	$$⊢j=k\to F\left(j\right)=F\left(k\right)$$
10	9	cbvsumv	$$⊢\sum _{j\in Z}F\left(j\right)=\sum _{k\in Z}F\left(k\right)$$
11	3	sumeq2dv	$$⊢\phi \to \sum _{k\in Z}F\left(k\right)=\sum _{k\in Z}A$$
12	10 11	syl5eq	$$⊢\phi \to \sum _{j\in Z}F\left(j\right)=\sum _{k\in Z}A$$
13	8 12	breqtrrd	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{j\in Z}F\left(j\right)$$
14	3 4	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
15	6 3	breqtrrd	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le F\left(k\right)$$
16	1 2 13 14 15	iserge0	$$⊢\phi \to 0\le \sum _{j\in Z}F\left(j\right)$$
17	16 12	breqtrd	$$⊢\phi \to 0\le \sum _{k\in Z}A$$