Theorem isumrpcl

Description: The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumrpcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumrpcl.2	$$⊢W={\mathbb{Z}}_{\ge N}$$
3		isumrpcl.3	$$⊢\phi \to N\in Z$$
4		isumrpcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		isumrpcl.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in {ℝ}^{+}$$
6		isumrpcl.6	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
7	3 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
8		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
9	7 8	syl	$$⊢\phi \to N\in \mathbb{Z}$$
10		uzss	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
11	7 10	syl	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
12	11 2 1	3sstr4g	$$⊢\phi \to W\subseteq Z$$
13	12	sselda	$$⊢\left(\phi \wedge k\in W\right)\to k\in Z$$
14	13 4	syldan	$$⊢\left(\phi \wedge k\in W\right)\to F\left(k\right)=A$$
15	5	rpred	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
16	13 15	syldan	$$⊢\left(\phi \wedge k\in W\right)\to A\in ℝ$$
17	4 5	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in {ℝ}^{+}$$
18	17	rpcnd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
19	1 3 18	iserex	$$⊢\phi \to \left(seqM\left(+,F\right)\in \mathrm{dom}⇝\leftrightarrow seqN\left(+,F\right)\in \mathrm{dom}⇝\right)$$
20	6 19	mpbid	$$⊢\phi \to seqN\left(+,F\right)\in \mathrm{dom}⇝$$
21	2 9 14 16 20	isumrecl	$$⊢\phi \to \sum _{k\in W}A\in ℝ$$
22		fveq2	$$⊢k=N\to F\left(k\right)=F\left(N\right)$$
23	22	eleq1d	$$⊢k=N\to \left(F\left(k\right)\in {ℝ}^{+}\leftrightarrow F\left(N\right)\in {ℝ}^{+}\right)$$
24	17	ralrimiva	$$⊢\phi \to \forall k\in ZF\left(k\right)\in {ℝ}^{+}$$
25	23 24 3	rspcdva	$$⊢\phi \to F\left(N\right)\in {ℝ}^{+}$$
26		seq1	$$⊢N\in \mathbb{Z}\to seqN\left(+,F\right)\left(N\right)=F\left(N\right)$$
27	9 26	syl	$$⊢\phi \to seqN\left(+,F\right)\left(N\right)=F\left(N\right)$$
28		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
29	9 28	syl	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge N}$$
30	29 2	eleqtrrdi	$$⊢\phi \to N\in W$$
31	16	recnd	$$⊢\left(\phi \wedge k\in W\right)\to A\in ℂ$$
32	2 9 14 31 20	isumclim2	$$⊢\phi \to seqN\left(+,F\right)⇝\sum _{k\in W}A$$
33	12	sseld	$$⊢\phi \to \left(m\in W\to m\in Z\right)$$
34		fveq2	$$⊢k=m\to F\left(k\right)=F\left(m\right)$$
35	34	eleq1d	$$⊢k=m\to \left(F\left(k\right)\in {ℝ}^{+}\leftrightarrow F\left(m\right)\in {ℝ}^{+}\right)$$
36	35	rspcv	$$⊢m\in Z\to \left(\forall k\in ZF\left(k\right)\in {ℝ}^{+}\to F\left(m\right)\in {ℝ}^{+}\right)$$
37	33 24 36	syl6ci	$$⊢\phi \to \left(m\in W\to F\left(m\right)\in {ℝ}^{+}\right)$$
38	37	imp	$$⊢\left(\phi \wedge m\in W\right)\to F\left(m\right)\in {ℝ}^{+}$$
39	38	rpred	$$⊢\left(\phi \wedge m\in W\right)\to F\left(m\right)\in ℝ$$
40	38	rpge0d	$$⊢\left(\phi \wedge m\in W\right)\to 0\le F\left(m\right)$$
41	2 30 32 39 40	climserle	$$⊢\phi \to seqN\left(+,F\right)\left(N\right)\le \sum _{k\in W}A$$
42	27 41	eqbrtrrd	$$⊢\phi \to F\left(N\right)\le \sum _{k\in W}A$$
43	21 25 42	rpgecld	$$⊢\phi \to \sum _{k\in W}A\in {ℝ}^{+}$$