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={\mathbb{Z}}_{\ge M}$$
	iserge0.2	$$⊢\phi \to M\in \mathbb{Z}$$
	iserge0.3	$$⊢\phi \to seqM\left(+,F\right)⇝A$$
	iserge0.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
	iserge0.5	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le F\left(k\right)$$
Assertion	iserge0	$$⊢\phi \to 0\le A$$

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		iserge0.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		iserge0.3	$$⊢\phi \to seqM\left(+,F\right)⇝A$$
4		iserge0.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
5		iserge0.5	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le F\left(k\right)$$
6		serclim0	$$⊢M\in \mathbb{Z}\to seqM\left(+,\left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\right)⇝0$$
7	2 6	syl	$$⊢\phi \to seqM\left(+,\left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\right)⇝0$$
8		simpr	$$⊢\left(\phi \wedge k\in Z\right)\to k\in Z$$
9	8 1	eleqtrdi	$$⊢\left(\phi \wedge k\in Z\right)\to k\in {\mathbb{Z}}_{\ge M}$$
10		c0ex	$$⊢0\in \mathrm{V}$$
11	10	fvconst2	$$⊢k\in {\mathbb{Z}}_{\ge M}\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\left(k\right)=0$$
12	9 11	syl	$$⊢\left(\phi \wedge k\in Z\right)\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\left(k\right)=0$$
13		0re	$$⊢0\in ℝ$$
14	12 13	eqeltrdi	$$⊢\left(\phi \wedge k\in Z\right)\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\left(k\right)\in ℝ$$
15	12 5	eqbrtrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left({\mathbb{Z}}_{\ge M}\times \left\{0\right\}\right)\left(k\right)\le F\left(k\right)$$
16	1 2 7 3 14 4 15	iserle	$$⊢\phi \to 0\le A$$